[Python]Z3で数独パズルを解くをリファクタリング

#本日は

数独のソルバーを紹介している
[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