数独は非常に SAT に変換しやすい問題です。全部参考文献 *1 に載っている内容ですが、なるべくわかりやすく説明してみます。ちょっと長いです。
SAT とは
まず SAT をごく簡単に説明します。すでに SAT を知っている人はここは読み飛ばしてください。
命題論理式の形の一つに乗法標準形のというのがあります。変数か変数の否定 (リテラルと言います) を or だけでつないだ式 (節と言います) を and だけでつないだ論理式のことを言います。つまり以下みたいな形です。
( a1 or !a2 or ... or an) and ( b1 or !b2 or ... or !bn) and ... and (!z1 or z2 or ... or !zn)
SAT は「a1 や zn などの変数にうまく true か false を代入して、上の式全体を true にできるか」という問題です。たとえば、
(a or b) and (!a or b) and (a or !b)
という論理式は a = b = true のとき全体として true になるので、Yes が解答になります。
(a or b) and (!a or b) and (a or !b) and (!a or !b)
という論理式は a と b がどういう値でも true にはできないので、No が解答になります。
SAT ソルバは SAT を解いてくれるプログラム・ライブラリです。多くの SAT ソルバは解答が Yes の場合、その論理式を true にするような変数割り当てを 1 つ教えてくれます。
数独
簡単のため 4x4 の数独問題で説明します。数独のルールを確認しますと、
- 各マスに 1 から 4 のいずれかが入る
- 各行に同じ数字が 2 回以上現れない
- 各列に同じ数字が 2 回以上現れない
- 各ブロックに同じ数字が 2 回以上現れない
だけです。非常にシンプルですね。以下例題。
. .|. 4 . .|1 2 ---+---- . 1|4 3 4 3|2 1
数独の SAT encoding
SAT ソルバを使って問題を解くということは、
- 数独のルールと盤面を乗法標準形の論理式に変換して、
- それを SAT ソルバに与えて、
- 得られた変数割り当てから盤面の形 (つまり解答) に逆変換する、
ということです。最初の変換を考えるところが肝になります。
まず数独のルールを論理式に変換します。各マスに次のように名前を振ります。
a b|c d e f|g h ---+--- i j|k l m n|o p
各マスに対して 4 つの変数を割り当てます。4x4 ならマスは 16 個あるので、64 個の変数を用意することになります。a のマスには a1 、a2 、a3 、a4 を割り当てたとします。他のマスも同様に。それぞれの意味を以下のように決めます。
- a1 が true のとき、a のマスには 1 が入る
- a2 が true のとき、a のマスには 2 が入る
- a3 が true のとき、a のマスには 3 が入る
- a4 が true のとき、a のマスには 4 が入る
ここで、「各マスに 1 から 4 のいずれかが入る」という条件は、以下の節で表現できます。
(a1 or a2 or a3 or a4)
同じ条件を各マスに対して設定しますので、16 個の節が得られます。
次に、「各行に同じ数字が 2 回以上現れない」です。この条件は
- 各行に 1 が 2 回以上現れない
- 各行に 2 が 2 回以上現れない
- 各行に 3 が 2 回以上現れない
- 各行に 4 が 2 回以上現れない
の 4 つの条件に分解できます。a から d の行に対して、1 つ目の条件は 6 つの節からなる論理式になります。
(!a1 or !b1) and (!a1 or !c1) and (!a1 or !d1)
and (!b1 or !c1) and (!b1 or !d1)
and (!c1 or !d1)ちょっとややこしいですが、a1 から d1 のどれか 2 つが同時に true だった場合、どれかの節が false になるようになっています。
他の数字、他の行に対しても同様に論理式を作れます。6 (節) × 4 (数字の種類の数) × 4 (行の数) で、96 個の節になります。また、「各列に同じ数字が 2 回以上現れない」「各ブロックに同じ数字が 2 回以上現れない」もこれと同様に、それぞれ 96 個の節に変換できます。
以上で得られた 16 ＋ 96 × 3 = 304 個の節を and でつなげた式が、数独のルールを表す論理式になります。
次に数独の各問題の盤面を論理式に直す方法ですが、これは簡単です。すでに埋められているマスの数字に対応する変数をそのまま and でつなげていけばいいだけです。
たとえば前述の例題では d のマスがあらかじめ 4 だとわかっているので d4 は必ず true 、同様に g1 が true 、h2 が true 、……、p1 が true です。したがって、
(数独のルールを表す論理式) and d4 and g1 and h2 and ... and p1
が、求めていた乗法標準形の論理式ということになります。
この論理式を SAT ソルバに与えると、SAT ソルバはこの論理式を true にする変数割り当てを教えてくれます (もしそういう変数割り当てはないと言われた場合、もともと解のない問題だったということになります) 。この変数割り当てから盤面に変換するのも簡単です。a1 が true なら a のマスには 1 を、a2 が true なら a のマスには 2 を入れていけばいいだけです。これで SAT ソルバを使って数独が解けたことになります。
最適化
上記の変換では数独の最小限のルールを変換したことになります。でも、普通の人は以下の補助ルールも暗黙のうちに仮定して解きます。
- 各マスに 1 から 4 の高々 1 つが入る
- 各行に各数字が最低 1 回は現れる
- 各列に各数字が最低 1 回は現れる
- 各ブロックに各数字が最低 1 回は現れる
これらは数独の最小限のルールから推論できる補助ルールなので、必須ではありません。しかしこれらのルールを論理式に追加することで、SAT ソルバが余計な探索を枝刈りできるようになります。
これらの補助ルールを節に変換する方法は上記とほぼ同じなので省略します。あと 4x4 や 9x9 程度の問題は、今の SAT ソルバなら補助ルールなしでも一瞬で解けるようです (Core 2 で 0.01 秒とかそのくらい) 。
別解探索
上記の方法で 1 つの解が得られたとして、別解がないかどうかをチェックすることも SAT ソルバでできます。すでに得られた解と一致する変数割り当てを禁止する節を追加します。たとえば前述の例題の解答は以下になります。
1 2|3 4 3 4|1 2 ---+--- 2 1|4 3 4 3|2 1
この解は、「a1 が true 、b2 が true 、c3 が true 、 d4 が true 、e3 が true 、……、p1 が true」という変数割り当てで表現されています。したがって、
(数独のルールを表す論理式) and (盤面を表す論理式) and (!a1 or !b2 or !c3 or !d1 or !e3 or ... or !p1)
という論理式を true にする変数割り当てが存在するかどうかを判定して、存在しなければ別解はないということになります。
おまけ
4x4 限定で基本部分だけ (最適化・別解探索なし) を実装したコードです。
# for ruby 1.9 require "minisat" solver = MiniSat::Solver.new # 例題 puzzle = [ [0, 0, 0, 4], [0, 0, 1, 2], [0, 1, 4, 3], [4, 3, 2, 1] ] # 各マスに 4 つの変数を割り当てる field = (0...4).map do (0...4).map do (0...4).map { solver.new_var } end end # 各マスに 1 から 4 のいずれかが入る field.each do |row| row.each do |num| solver << num end end # 各行に同じ数字が 2 回以上現れない field.each do |row| row.transpose.each do |vars| vars.combination(2) do |x, y| solver << [-x, -y] end end end # 各列に同じ数字が 2 回以上現れない field.transpose.each do |row| row.transpose.each do |vars| vars.combination(2) do |x, y| solver << [-x, -y] end end end # 各ブロックに同じ数字が 2 回以上現れない field.each_slice(2) do |row1, row2| row1.zip(row2).each_slice(2) do |box| box.flatten(1).transpose.each do |vars| vars.combination(2) do |x, y| solver << [-x, -y] end end end end # すでに埋まっている数字の変数を追加する puzzle.zip(field) do |prow, vrow| prow.zip(vrow) do |pnum, vnum| solver << vnum[pnum - 1] if pnum >= 1 end end # SAT を解く solver.solve || exit(1) # 盤面に逆変換する field.each do |row| line = row.map do |num| (1..4).find {|i| solver[num[i - 1]] } end puts line.join(" ") end
*1:I. Lynce, and J. Ouaknine. Sudoku as a SAT Problem. Proceedings of the Ninth International Symposium on Artificial Intelligence and Mathematics (AIMATH 2006), Jan. 2006
