@article{oai:ipsj.ixsq.nii.ac.jp:00169443,
 author = {田村, 直之 and 宋, 剛秀 and 番原, 睦則 and TAMURA, Naoyuki and SOH, Takehide and BANBARA, Mutsunori},
 issue = {8},
 journal = {情報処理},
 month = {Jul},
 note = {数独やナンバーリンクなどのパズルを題材として取り上げ，SATソルバーを用いてこれらのパズルを解く方法について説明する．SATソルバーは，与えられた連言標準形の命題論理式（CNF式）を満たす解を探索するプログラムである．近年になって大幅な性能向上が実現され，最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている．このことを背景とし，さまざまな問題をCNF式に変換（符号化） しSAT ソルバーで解を求める手法が注目を集めている．本稿では，パズルを題材とすることで，この手法について分かりやすく解説する．},
 pages = {710--715},
 title = {SAT技術の進化と応用 〜パズルからプログラム検証まで〜：2．SATとパズル -問題をいかにSATソルバーで解くか-},
 volume = {57},
 year = {2016}
}