Bibliographic Information
- Other Title
-
- SAT技術の進化と応用 〜パズルからプログラム検証まで〜:2.SATとパズル -問題をいかにSATソルバーで解くか-
- SAT ト パズル : モンダイ オ イカニ SAT ソルバー デ トク カ
- SAT Evolution and Applications:2. Satisfiability and Puzzles - How to Solve Problems with a SAT Solver -
Search this article
Abstract
数独やナンバーリンクなどのパズルを題材として取り上げ,SATソルバーを用いてこれらのパズルを解く方法について説明する.SATソルバーは,与えられた連言標準形の命題論理式(CNF式)を満たす解を探索するプログラムである.近年になって大幅な性能向上が実現され,最新のSATソルバーは百万個の変数を含む問題でも取り扱えるようになっている.このことを背景とし,さまざまな問題をCNF式に変換(符号化) しSAT ソルバーで解を求める手法が注目を集めている.本稿では,パズルを題材とすることで,この手法について分かりやすく解説する.
Journal
-
- 情報処理
-
情報処理 57 (8), 710-715, 2016-07-15
東京 : 情報処理学会 ; 1960-
- Tweet
Keywords
Details 詳細情報について
-
- CRID
- 1050001337907131392
-
- NII Article ID
- 40020914080
-
- NII Book ID
- AN00116625
-
- ISSN
- 04478053
-
- NDL BIB ID
- 027555321
-
- Text Lang
- ja
-
- Article Type
- departmental bulletin paper
-
- Data Source
-
- IRDB
- NDL
- CiNii Articles