SATソルバーで数独を解く
今週のタイムライン
エネルギーを奪った出来事（悲しくなった・不幸になったなど）
- わからないことをその場で質問できなかった（時間がなかったのもあったが）（水曜日）
- レトロスペクティブ（チームでのふりかえり）が時間を書けている割に効果が出ていない感（木曜日）
エネルギーを与えた出来事（幸せになった・安心した）
- キムチ作り（日曜日）
- 先輩とペア作業をして学ぶことが多い（Unit test, Git, RxJava）
- Think Clearlyを読み始めた（水曜日）
- 大きなタスクを完了にできた（水曜日）
- e2eによって問題の解決方法が誤っていることに気づけた（金曜日）
- SATソルバーで数独を解けた（金曜日）
戸惑った出来事や疑問に思った出来事
特になし
話したいこと
- SATソルバーで数独を解けた（金曜日）
SATソルバーで数独を解く
最近SATについて理解する必要があり、勉強のために数独を解かせてみました。SATは充足可能性問題（Satisfiability problem）のことで、たくさんの論理式を与えて、それらの論理式がすべて真となるような変数を探すという問題です。
具体例を示す前に説明に必要な用語があるので説明します。
具体的には以下のような問題があったとします。
以下の条件を満たすx, y, zを求めよ
- xまたはyが真である
- xが偽である又はzが真である
- yは偽である
この時x, y, zがリテラル、xまたはyが真であるが節、1,2,3の条件を全部で連言標準形のことを指しています。この問題をSATソルバーを使って解くとすると以下のようなコードで解くことができます。
from pysat.solver import Minisat22 x=1 y=2 z=3 solver = Minisat22() clause1 = [x, y] # x or y = xまたはyが真である clause2 = [-x, z] # !x or z = xが偽である又はzが真である clause3 = [-y] # !y = yは偽である solver.add_clause(clause1) solver.add_clause(clause2) solver.add_clause(clause3) solver.solve() solver.get_model() # -> [1, -2, 3]
最後に出てきた[1, -2, 3]はxが真、yが偽、zが真を表しています。
実際にこの答えで与えられた条件をすべて満たしています。
SATでは上記のように条件を節に置き換えることができれば問題を解くことができます。 この要領で数独も解くことができるらしかったので、実際にプログラムを書いて解いてみました。
9×9の数独の条件としては以下のようなものがあります。
- 各マスには1~9のいずれかが入る
- 各行に少なくとも1回以上1~9が入る
- 各列に少なくとも1回以上1~9が入る
- 各ブロック（3×3の区域）に少なくとも1回以上1~9が入る
- 各マスに異なる数字が同時に入らない
- 各行に同じ数字が入らない
- 各列に同じ数字が現れない
- 各ブロックに同じ数字が現れない
- すでに埋まっている値はそのままである
これらをすべて節として表現し、SATソルバーに与えてあげれば数独が解けるはず。 それでは以下のような問題を考えましょう。
-,-,-,-,-,-,-,7,- 1,-,5,-,3,6,4,-,9 -,7,4,9,-,-,5,-,- -,-,-,-,-,5,8,-,- -,1,-,3,-,-,-,-,5 7,-,-,-,-,8,1,-,- 6,4,-,-,-,-,-,-,7 -,3,-,6,2,-,-,8,4 -,-,-,5,9,-,-,-,3
まずは各マスに1~9が入るかどうかという変数が必要なので考えます。 9×9の数独で、各マスに1~9が入るので9×9×9個のリテラルが必要です。 e.g. 一番左上でのマスに1が入るかどうか、一番左上でのマスに2が入るかどうか...
具体的には各マスにユニークな数字を割り当ててあげました。
class LiteralGenerator: def __init__(self): self.idx = 0 def next(self): self.idx += 1 return self.idx gen = LiteralGenerator() net = [] for i in range(9): matrix = [] for j in range(9): row = [gen.next() for k in range(9)] matrix.append(row) net.append(matrix) # net[行][列][数値]
一番上の行の7はnet[0][7][6]で70ということになります。
（ここを理解するのに苦労しました。）
それではここから一つ一つの条件を考えていきます。
1. 各マスには1~9のいずれかが入る
例えば左上のマスに1~9のいずれかが入ることを表現したければ、
net[0][0][0] or net[0][0][1] or ... or net[0][0][8]
で表現できます。これを全マス分の節を作る必要があります。
cnf = CNF() for row in range(9): for col in range(9): cnf.append([net[row][col][num] for num in range(9)])
2. 各行に少なくとも1回以上1~9が入る
例えば1行目に少なくとも1が1回以上入ることを表現したければ、
net[0][0][0] or net[0][1][0] or ... or net[0][8][0]
で表現できます。これを全行、全数字分の節を作る必要があります。
for num in range(9): for row in range(9): cnf.append([net[row][col][num] for col in range(9)])
3. 各列に少なくとも1回以上1~9が入る
例えば1列目に少なくとも1が1回以上入ることを表現したければ、
net[0][0][0] or net[1][0][0] or ... net[8][0][0]
で表現できます。これを全列、全数字分の節を作る必要があります。
for num in range(9): for col in range(9): cnf.append([net[row][j][num] for row in range(9)])
4. 各ブロック（3×3の区域）に少なくとも1回以上1~9が入る
例えば左上のブロックに関して少なくとも1が1回以上入ることを表現したければ、
net[0][0][0] or ... or net[1][1][0] or net[2][2][0]
で表現できます。これを全ブロック、全数字分の節を作る必要があります。 （この条件は実装するのが結構迷った）
for num in range(9): for j in range(9): cnf.append([net[(j//3)*3+(k//3)][j%3*3+k%3][num] for k in range(9)]) # 行は0, 1, 2 × 3, 3, 4, 5 × 3, ...と変化する必要がある # 列は0, 0, 0, 1, 1, 1, 2, 2, 2, ...と変化する必要がある
5. 各マスに異なる数字が同時に入らない
左上のマスに1と2が同時に入らないこと表現したければ、
-net[0][0][0] or -net[0][0][1]
で表現できます。ちょっと分かりづらいですが、net[0][0][0] and net[0][0][1]の否定を表したいのでド・モルガンの法則を用いてorになおすと上記のようになります。
これを全マス分の節を作る必要があります。
for row in range(9): for col in range(9): for num1 in range(9): for num2 in range(num1+1, 9): cnf.append([-net[row][col][num1], -net[row][col][num2])
6. 各行に同じ数字が入らない
1行目の一番左とその右のマスに1が複数回現れないことを表現したければ、
-net[0][0][0] or -net[0][1][0]
で表現できます。全行、全数字分の節を作る必要があります。
for num in range(9): for row in range(9): for col1 in range(9): for col2 in range(col1+1, 9): cnf.append([-net[row][col1][num], -net[row][col2][num])
7. 各列に同じ数字が現れない
1列目に一番上とその下のマスに1が複数回現れないことを表現したければ、
-net[0][0][0] or -net[1][0][0]
で表現できます。全列、全数字分の節を作る必要があります。
for num in range(9): for col in range(9): for row1 in range(9): for row2 in range(row1+1, 9): cnf.append([-net[row1][col][num], -net[row2][col][num])
8. 各ブロックに同じ数字が現れない
左上のブロックの左上とその右に1が複数回現れないことを表現したければ、
-net[0][0][0] or -net[0][1][0]
で表現できます。全ブロック、全数字分の節を作る必要があります。
for i in range(9): for j in range(9): for k in range(j+1, 9): row1 = (i//3)*3+j//3 row2 = (i//3)*3+k//3 col1 = i%3*3+j%3 col2 = i%3*3+k%3 cnf.append([-net[row1][col1][0], -net[row2][col2][0]])
9. すでに埋まっている値はそのままである
今回与えられた問題は以下のようなものなので、数字が入っている部分に関して節を作っていきます。
-,-,-,-,-,-,-,7,- 1,-,5,-,3,6,4,-,9 -,7,4,9,-,-,5,-,- -,-,-,-,-,5,8,-,- -,1,-,3,-,-,-,-,5 7,-,-,-,-,8,1,-,- 6,4,-,-,-,-,-,-,7 -,3,-,6,2,-,-,8,4 -,-,-,5,9,-,-,-,3
右上の7はnet[0][7][6]、1行2列目の1はnet[1][0][0]という感じで表現してきます。
ここの処理は詳しい処理は省略しちゃいます。
全部の節が揃った！
この数独を解くために作成した節はすべてで9426個でリテラルは最初に述べたとおり729個でした。実際に解いてみると、
solver = Minisat22() solver.append_formula(cnf.clauses, no_return=False) solver.solve() ans = np.array(solver.get_model()).reshape(9, 9, 9) ans = ans[ans > 0].reshape(9, 9) ans = ans % 9 print(np.where(ans == 0, 9, ans)) -> array([[9, 6, 2, 4, 5, 1, 3, 7, 8], [1, 8, 5, 7, 3, 6, 4, 2, 9], [3, 7, 4, 9, 8, 2, 5, 6, 1], [4, 9, 6, 1, 7, 5, 8, 3, 2], [2, 1, 8, 3, 6, 9, 7, 4, 5], [7, 5, 3, 2, 4, 8, 1, 9, 6], [6, 4, 9, 8, 1, 3, 2, 5, 7], [5, 3, 1, 6, 2, 7, 9, 8, 4], [8, 2, 7, 5, 9, 4, 6, 1, 3]])
解けた！すごい！
最後に
学んだことをまとめようとするとついつい長くなっちゃいました。最近読んだ本とかの感想や先輩から学んだことも書きたかったけど、書くのが疲れちゃいました笑 週末じゃない時にも書いて投稿しようかなぁ。。。
全然関係ないけど、今週のキムチ作りの時に食べたユッケジャンクッパが美味しかった！
