本日は
数独のソルバーを紹介している
[Python]Z3で数独パズルを解く
のソルバーをクラス化させてみました．理由としては，
- 再現実験として試したかった（楽しそうだった）
- これをベースに簡単なGUIアプリを作ってみたかったこと
- そのためにクラス化によるリファクタリングでコードの再利用性を高めたかった．
z3 のインストール
Macの場合
$ pip install z3-solver
でインストールが可能になります．
ビルドに時間がかかります．ゆっくり待ちましょう．
実装例
z3solver
import z3
from itertools import product
grid = lambda i, j: z3.Int("grid[%d,%d]" % (i, j))
class Z3Solver(z3.Solver):
GRID_SIZE = 9
SUB_GRID_SIZE = 3
def __init__(self, problem):
super(Z3Solver, self).__init__()
self.problem = problem
self._set_problem()
def solve(self):
self._set_restriction()
return self.check()
def _set_problem(self):
N = Z3Solver.GRID_SIZE
for i, j in product(range(N), range(N)):
if self.problem[i][j] > 0:
self.add(grid(i, j) == self.problem[i][j])
def _set_restriction(self):
N = Z3Solver.GRID_SIZE
B = Z3Solver.GRID_SIZE//Z3Solver.SUB_GRID_SIZE
SUB_GRID_SIZE = Z3Solver.SUB_GRID_SIZE
#set initial value
self.add(*[1 <= grid(i, j) for i, j in product(range(N), repeat=2)])
self.add(*[grid(i, j) <= 9 for i, j in product(range(N), repeat=2)])
#distinct w.r.t col
for row in range(N):
self.add(z3.Distinct([grid(row, col) for col in range(N)]))
#distinct w.r.t row
for col in range(N):
self.add(z3.Distinct([grid(row, col) for row in range(N)]))
#distinct
for row in range(B):
for col in range(B):
block = [grid(B*row+i, B*col+j)
for i, j in product(range(SUB_GRID_SIZE), repeat=2)]
self.add(z3.Distinct(block))
def solve_sudoku(problem):
solver = Z3Solver(problem)
result = solver.solve()
if result == z3.sat:
model = solver.model()
# print result
for i in range(Z3Solver.GRID_SIZE):
for j in range(Z3Solver.GRID_SIZE):
print("%d " % model[grid(i, j)].as_long(), end="")
print("")
print("")
else:
print(result)
def main():
problem1 = [[0, 0, 0, 0, 0, 0, 0, 0, 0],
[0, 0, 0, 0, 0, 1, 0, 8, 0],
[6, 4, 0, 0, 0, 0, 7, 0, 0],
[0, 0, 0, 0, 0, 3, 0, 0, 0],
[0, 0, 1, 8, 0, 5, 0, 0, 0],
[9, 0, 0, 0, 0, 0, 4, 0, 2],
[0, 0, 0, 0, 0, 9, 3, 5, 0],
[7, 0, 0, 0, 6, 0, 0, 0, 0],
[0, 0, 0, 0, 2, 0, 0, 0, 0]]
solve_sudoku(problem1)
problem2 = [[0, 0, 0, 0, 0, 0, 0, 3, 9],
[0, 0, 0, 0, 0, 1, 0, 0, 5],
[0, 0, 3, 0, 5, 0, 8, 0, 0],
[0, 0, 8, 0, 9, 0, 0, 0, 6],
[0, 7, 0, 0, 0, 2, 0, 0, 0],
[1, 0, 0, 4, 0, 0, 0, 0, 0],
[0, 0, 9, 0, 8, 0, 0, 5, 0],
[0, 2, 0, 0, 0, 0, 6, 0, 0],
[4, 0, 0, 7, 0, 0, 0, 0, 0]]
solve_sudoku(problem2)
if __name__ == '__main__':
main()
簡単な変更点として
-
z3を継承して数独のソルバーとするクラスを実装した． - 入力データフォーマットを整数値を持つ二重配列リストにした（不定部分を0にする）
- 変数をアンダースコアを用いて単語の区切りをするようにした．
- 多重ループを
itertool.productを用いて見た目の行数を減らす． - 制約条件を設定する部分を一つにまとめる
制約条件についてはどうやら
self.add(*[1 <= grid(i, j) <=9 for i, j in product(range(N), range(N))])
という書き方はダメみたい．z3.addしたときに解析が失敗します．
複数の条件を一気に add したい場合 add したい対象をリストに入れて
self.add(*[P,Q,R,S,T,U])
のようにリストの前に*をつけて展開させるのがミソ
この後は
GUIアプリを作ってみたい．（また後日）
追記：アルファ版作りました．ー＞ https://qiita.com/SatoshiTerasaki/items/e98c9a1c88c0280f54c4