SAT ソルバで数独を解く方法 - まめめも

数独は非常に SAT に変換しやすい問題です。全部参考文献 *1 に載っている内容ですが、なるべくわかりやすく説明してみます。ちょっと長いです。 SAT とは まず SAT をごく簡単に説明します。すでに SAT を知っている人はここは読み飛ばしてください。 命題論理式の形の一つに乗法標準形のというのがあります。変数か変数の否定 (リテラルと言います) を or だけでつないだ式 (節...

http://d.hatena.ne.jp/ku-ma-me/20080108/p1

これはいい
sudokuはNP-complete。その他かなりディープな詳細 → wikipedia "Mathematics of Sudoku" http://en.wikipedia.org/wiki/Mathematics_of_Sudoku
大学時代に並列SATソルバのアルゴリズム研究してたのが懐かしい

http://b.hatena.ne.jp/entry/http://d.hatena.ne.jp/ku-ma-me/20080108/p1