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

３月５日木曜日、晴れ

どうやら花粉がひどい。風も強かった。（風が強いから花粉の飛散も激しかったという流れが正しい？）

＊　＊　＊

バグを直し、確認用のビルドを仕掛け、その間に次のバグを直して……　とやっていたらブランチを新しくするのを忘れ出しておいたプルリクエストに別の修正のコミットを積んでしまう。
作業を並行してやりすぎて頭がウニのようになっている。ちょっとオーバーヒート気味である。休ませないといけない。

＊　＊　＊

昨晩の続きで SAT ソルバーに食わせる制約条件の洗い出し。

１マスに入る９つの数の制約は、少なくともひとつは真になるという条件がひとつ。そして同時に真になるのは高々ひとつという条件。これは２つの命題の否定の和として表現できる。９つの数字から２つ取り出す組み合わせは３６通り。あわせて３７。８１マスあるので２９９７の制約条件。

行、列、箱とで同じように制約を数え上げられるので２９９７×４、全部で１１９８８通りの制約が出る。

ところでペアの組み合わせを見たときに、行と箱、列と箱には同じペアの組み合わせが現れる。機械的に重複を削除したところ、相異なる制約は１０５３０通りだった。

命題変数は８１×９の７２９個。（制約なしなら２の７２９乗というとんでもない桁の組み合わせが表現できる）
これに１０５３０通りの制約が加わり、さらに事前に置かれる２０〜３０の数字の制約を課して、そうするとたった１つの答えが定まる。

数独ってやっぱり面白い。