SATソルバーで25×25のナンプレがたった20秒で解かれてしまった

前回、SATについて簡単過ぎる紹介をした。
もっと詳しく知りたい場合は、神戸大学情報基盤センターの田村教授の資料 情報基礎特論:制約プログラミング入門 （PDF, 98ページ）が相当詳しい。

SATには、制御文がない。つまり、if-else, while, for,…などの文が存在しない。
存在するのは、定義文、条件文だけである。
つまり、定義の範囲で、条件を全て満たす変数の値を探すだけである。
もちろん、条件を満たす解が１組以上ある場合もあるが、解の個数を、解なし(0)、解１(ユニーク解)、複数解（多重解）の区別もしてくれたりする。

さて、こんなSATは、どうやって問題を解いているだろうか。
結論から言うと、最終的には虱潰しをやっているだけである。
しかし、途中で検索を省略できる箇所、早々に決まってしまう箇所、選択肢が非常に狭められる場合などを考慮し、相当高速に虱潰しができるようになっている。

それでも、さすがに25×25のナンプレを調べつくすのには相当の時間がかかると予想した。

神戸大学の田村教授に16×16の問題を解いてもらったときの時間が

real    0m3.311s
user    0m5.244s
sys     0m0.280s

20×20の問題を解いてもらったときの時間が

real    0m5.079s
user    0m7.312s
sys     0m0.600s

であった。
組み合わせ問題なので、サイズが大きくなると急激に時間がかかるようになるものだが、マスの総数の増加割合よりやや時間がかかる程度であった。 これなら、25×25も解かれてしまうかも知れない。
25×25のヒント数の少ない問題を作るのは、非常に困難で、コンピュータリソースをやたらに食う。

25×25の問題を送ったら、1時間余したら返信があり、なんと

real    0m17.693s
user    0m21.312s
sys     0m0.332s

という短い時間の間に解かれてしまったのだった。 最近のSATの性能向上には目を見張るものがある。 SATは、明示的な、手筋のような解き方をプログラミングする必要がないので、解法アルゴリズムがまったく思いつかないような場合に有効な方法だ。 このまま高性能化が進むと、アルゴリズムを考えず、とりあえずSATに探させれば良い、と考えるようになりそうだ。

いや、SATの開発者は、効率向上のために、ものすごくアルゴリズムを最適化しているはずだ。