SAT solverで「数独」「美術館」「ひとりにしてくれ」を解きました。
めっちゃ楽しかったので準急に多謝だー。（JOI春合宿で講義をしてくれた）
準備
SAT solverをインストールしましょう。
僕はminisatにしました。（なんか入れるのに苦労したけど）
SATを知らない人は適当に調べましょう。
流れとしては、
- パズルを連言標準形(CNF)の論理式にして
- SAT solverに投げて
- ビジュアライズする
って感じです。
数独
多分一番簡単です。
「x1,x2,...,x9 のうち、ちょうど１つだけがtrue」
という式が書ければ勝ちです。これは、
- x1 or x2 or ... or x9 （１つ以上であるという制約）
- 全てのi,jのペアについて、!xi or !xj （２つ以上ないという制約）
で実現できます。
あとは、X_i,j,k（i行目j列目がkであるならtrue）という変数を使って
- 行にちょうど１つだけkがある
- 列にちょうど１つだけkがある
- 3x3のグループにちょうど１つだけkがある
- 各マスにはちょうど１つだけ数が割り当てられている
という条件を書いてやればいいです。
美術館
これも基本的
変数は、X_i,j ＝ i行目j列目に明かりを置くならtrue です。
- 照らしあってはいけない
- 照らされていないマスがあってはいけない
- 黒マスに明かりがあってはいけない
- 周りに 0 個ある
- 周りに 1 個ある
- 周りに 3 個ある
- 周りに 4 個ある
は簡単（実際にプログラムとして書くのはちょっと面倒だけど）で、問題は
- 周りに 2 個ある
です。これは、
- どの３個を取り出してorを取ってもtrue
- どの３個を取り出して否定のorを取ってもtrue
の２つの条件にすると楽に書けます。
ちなみに、フィールドの周囲に番兵を置くとかなり実装が楽になります。
ひとりにしてくれ
- 各列に同じ数が２つ以上残ってはならない
- 黒マスが隣り合ってはならない
は簡単。
- 白マスは連結でなければならない
ひぇーっ！？こんなのできるんでしょうか？
かなりのパズルが連結性判定を必要とするので、これができないとなかなか厳しいです。
連結性判定は、いろいろな方法がありそうですが、僕が今回採用したのはBFSっぽい方法です。
イメージとしては、
- 適当に根を決めてBFSをするときの、各ステップでのvisitedの配列を変数にする。
という感じ。式を書く方針はこんな感じ。
- Y_i,j : i行目、j列目を黒く塗るならtrue
- X_i,j,k : i行目、j列目、BFSのkステップ目
- X_i,j,0 たちのうち、１つだけがtrue
- BFSの総ステップ数を T とすると、白マスの X_i,j,T は全部true
- 黒マスの X_i,j,k は全部false
- X_i,j,k+1 がtrueなら、X_ai,aj,kのうちいずれかはtrue（(ai,aj)は(i,j)に隣接するマス）
※「A ならば B」は 「!A or B」と変換できます
変数も節もO(マスの個数^2)個でいい感じです。
ちなみに、17x17のを１つやらせてみたら20秒で答えが出ました。感動！
