SAT技術の進化と応用 〜パズルからプログラム検証まで〜：2．SATとパズル -問題をいかにSATソルバーで解くか-

情報処理学会 Web Site

書誌事項

タイトル別名
  • SATとパズル : 問題をいかにSATソルバーで解くか
  • SAT ト パズル : モンダイ オ イカニ SAT ソルバー デ トク カ
  • SAT Evolution and Applications：2. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver -

この論文をさがす

抄録

数独やナンバーリンクなどのパズルを題材として取り上げ，SATソルバーを用いてこれらのパズルを解く方法について説明する．SATソルバーは，与えられた連言標準形の命題論理式（CNF式）を満たす解を探索するプログラムである．近年になって大幅な性能向上が実現され，最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている．このことを背景とし，さまざまな問題をCNF式に変換（符号化） しSAT ソルバーで解を求める手法が注目を集めている．本稿では，パズルを題材とすることで，この手法について分かりやすく解説する．

収録刊行物

  • 情報処理

    情報処理 57 (8), 710-715, 2016-07-15

    東京 : 情報処理学会 ; 1960-

キーワード

詳細情報 詳細情報について

問題の指摘

ページトップへ