SAT ソルバーで数独を解く（１）

３月４日水曜日、小雨

もう数年目のことになるか。
２５×２５サイズの数独を、自作のソルバーでは解けず悔しいおもいをしたのは。その後 SAT ソルバーというものを使うと解ける、という書き込みをどこかで目にしてずっと心に引っかかっていた。

こんなことをおもいだしたのは SMT ソルバーを使って証明器をつくるセミナーを５月に開催すると初谷さんから案内が来たから。（語感が似ていたので）

わからないのでちょっとだけ調べてみた。

SAT ソルバーは真か偽の二値を取る命題変数の組み合わせを与え、これを満たす値の組み合わせが存在するかどうかを見つけ出すアルゴリズム。これを進化させて述語論理を解けるようにしたのが SMT ソルバー、らしい。

＊　＊　＊

では SAT ソルバーでどのように数独を解くか？

それはこんな感じらしい。

Xrcn を「r 行 c 列に数字 n が入る」という命題だとする。１行２列に数字３が入ることを X123 とする、という感じ。
問題を見て数字が置かれているところは機械的に設定できて、標準的な数独なら３０前後の「真」と確定した命題が手に入る。

さて。数字が置かれていない場所をどうするか。

数独の特徴から例えばこんな制約が考えられる。
１行目のどこかに１が置かれる。これは X111 または X121 または X131 または…… X191。（９つの命題のうちどれかが真になれば成立）
一方で１行目には１が２つ以上現れることはない。つまり X111 かつ X121 が成り立つことはなく、 X111 かつ X131 も成り立たない。同様に X111 かつ X141、 X111 かつ X151、 X111 かつ X161、 X111 かつ X171、 X111 かつ X181、 X111 かつ X191 も成り立たない。 X121 と X131、 X121 と X141、……のようにペアを考えていずれも成り立たないという組み合わせ命題を列挙する。
同じように１行目のどこか１カ所に２が、３が、４が……と書ける。２行目、３行目と列挙していき、続いて同じようにして１列目、２列目、３列目と制約が書けて、加えて３×３の９つの箱についても制約が書ける。

そして大事なこととして、ある位置 rc には１から９までのいずれかひとつだけが入る。たとえば１行１列について、 X111 または X112 または X113 または…… X119 であり、 X111 かつ X112 はダメ、 X111 かつ X113 もダメ、…… X118 かつ X119 もダメ、までのペアの並び。これが９行９列まで延々と続く。

このようにして書き下したすべての命題を SAT ソルバーに入力すると答えが出る、らしい。

＊　＊　＊

仕組みはわかったので今週のうちに実際の問題を解けるか試してみたい。