SMT solver Yices を使ってみました。

研究で SMT (Satisfiability Modulo Theories) solver を使ってなにかしてみようというお話になったので、よくある数独ソルバーを作ってみました。
SMT solver とは、 SAT solver の便利バージョンのようなもので、変数、配列、関数などを定義できて、それらが満たすべき制約を等式や不等式を使って列挙して、それら制約を満たす変数、関数の割り当ての例を求めることができます。
SMT solver は SAT solver と密接に関係していて、数値の比較の式と、それらを結ぶ論理式に分けた時に、論理式を満たす真理値割り当てを求めるのに SAT solver が使われ、その真理値となる変数の割り当てを求めるのにSMT の理論が使われているようです。
例えば、(a == b and (a + b <= -1 or a + b >= 1)) を満たす変数の割り当てを知りたかったら、論理式を A and (B or C) として SAT solver にかけ, 真理値割り当てが A = true, B = false, C = true,を得られた場合、 {a == b, a + b > -1, a + b >= 1} を満たす変数の割り当てをさがして、これは {a = b = 1} が満たす (ここで失敗したら、SAT で違う割り当て探す。)、という感じのアルゴリズムだそうです。

以下のサイトを参考というか丸パ(ry しているので真新しいことはないけれど(；´∀｀)
SAT ソルバで数独を解く方法 - まめめも
SMT solver 入門 - suer のブログ

問題は、16x16の数独にしてみました。
3076 -- Sudoku
この問題は C++ でも単純な枝刈り探索だと何分待っても解が見つからず、数独を Exact cover 問題に変換して、Knuth's Algorithm X - Wikipedia を適用して枝刈り探索を効率化しないと、現実的な時間で解くことができない問題です。

問題の変換方法は先程の素晴らしいサイトにほとんど書いてあるので言うことはないのですが、いちおうプログラムを置いておきます。
https://github.com/halwhite/SmtSudoku16

実行時間は、数独の最小限のルール(行、列、ブロック内の変数は互いに異なる)のみを使った場合、4分くらいかかりましたが、すべてのnにたいして、各行、列、ブロック内のいずれかのマスはnと等しい、というヒントを追加した場合、2秒程度で終わり、その強力さがわかりました。
ちなみに、C++ で実装した Knuth's algorithm X で解いた場合、0.2秒程度で解けますが、結構しんどいです。