z3を使ってパズルを解く

Microsoft Researchの開発したSMT(Satisfiability modulo theories)を使ってパズルを解くことを試みる． パズルを計算機を使って解くのはプログラムの例題として，

n-queens を解く

n-queens は

まずは，z3というモジュールに含まれる定義を使うことを宣言する．

In [3]:
from z3 import *

記述をシンプルにするためにこのようにしたが，名前空間 (name space) をシンプルにすることを意図するなら， import z3 とした上で，z3.Var('x') などと記述することができる．

準備

nの初期値を設定する．また，solverを作る．

In [4]:
n = 10
solver = Solver()

これで，ソルバが作られる．

変数を作る

解くパズルは「変数」と「制約」で表現する． 「変数」としては，bool変数，整数変数などいろいろある．n-queensを表現する方法はいろいろあるが，まずは， n x n のマス square[y][x] にqueenが置かれている時に1, 置かれていない時に0になるようにしたい．

In [5]:
squares = [[Int('s_%d_%d' % (x, y)) for y in range(n)] for x in range(n)]

制約を書く

まずsquaresの要素は0以上1以下である．それを書く

In [6]:
for r in squares:
    for s in r:
        solver.add(0 <= s, s <= 1)

次に行ごとの和が1になっていることを書く．

In [7]:
for r in squares:
    solver.add(sum(r) == 1)

何気なく python の sum などを使っているが，これが正しい制約に変換されていることは， solver などとして，加えられた制約を表示させてみると分かる． 次に列ごとの和が1になっていることを書く．

In [8]:
for x in range(n):
    solver.add(sum(r[x] for r in squares) == 1)

斜め同士に駒が存在しないという制約も書いてみよう

In [9]:
for y0 in range(n):
    for x0 in range(n):
        for y1 in range(n):
            for x1 in range(n):
                if x1 != x0 and y1 != y0 and abs(x1 - x0) == abs(y1 - y0):
                    solver.add(squares[y0][x0] + squares[y1][x1] <= 1)

これが解を持つかどうかは solver.check() がsatを返すことで確認できる．

In [10]:
solver.check()
Out[10]:
sat

この時に変数にどのような割り当てが行われて制約が満たされたかは，solver.model() で確認できる．

In [11]:
solver.model()
Out[11]:
[s_2_4 = 0,
 s_4_3 = 0,
 s_7_2 = 1,
 s_7_7 = 0,
 s_9_2 = 0,
 s_9_8 = 0,
 s_1_9 = 0,
 s_5_1 = 0,
 s_6_1 = 0,
 s_5_5 = 0,
 s_1_4 = 0,
 s_6_6 = 1,
 s_3_5 = 0,
 s_3_4 = 1,
 s_7_4 = 0,
 s_7_6 = 0,
 s_9_5 = 0,
 s_2_3 = 0,
 s_5_8 = 0,
 s_4_2 = 0,
 s_5_7 = 0,
 s_5_4 = 0,
 s_3_1 = 0,
 s_6_9 = 0,
 s_2_2 = 0,
 s_1_7 = 0,
 s_2_5 = 0,
 s_2_9 = 0,
 s_3_6 = 0,
 s_7_3 = 0,
 s_6_4 = 0,
 s_4_6 = 0,
 s_8_7 = 0,
 s_8_6 = 0,
 s_6_3 = 0,
 s_6_5 = 0,
 s_6_2 = 0,
 s_2_7 = 0,
 s_4_4 = 0,
 s_4_9 = 0,
 s_4_1 = 0,
 s_5_2 = 0,
 s_2_1 = 0,
 s_3_8 = 0,
 s_3_2 = 0,
 s_4_8 = 0,
 s_5_3 = 0,
 s_2_6 = 0,
 s_7_1 = 0,
 s_8_3 = 0,
 s_4_7 = 1,
 s_3_7 = 0,
 s_1_3 = 1,
 s_3_9 = 0,
 s_7_5 = 0,
 s_8_4 = 0,
 s_8_5 = 1,
 s_7_9 = 0,
 s_9_7 = 0,
 s_9_1 = 1,
 s_1_1 = 0,
 s_2_8 = 0,
 s_8_8 = 0,
 s_1_2 = 0,
 s_1_8 = 0,
 s_8_1 = 0,
 s_4_5 = 0,
 s_6_7 = 0,
 s_8_9 = 0,
 s_9_3 = 0,
 s_8_2 = 0,
 s_9_9 = 0,
 s_9_6 = 0,
 s_3_3 = 0,
 s_6_8 = 0,
 s_7_8 = 0,
 s_1_5 = 0,
 s_5_9 = 1,
 s_1_6 = 0,
 s_5_6 = 0,
 s_9_4 = 0,
 s_9_0 = 0,
 s_8_0 = 0,
 s_7_0 = 0,
 s_6_0 = 0,
 s_5_0 = 0,
 s_4_0 = 0,
 s_3_0 = 0,
 s_2_0 = 1,
 s_1_0 = 0,
 s_0_0 = 0,
 s_0_9 = 0,
 s_0_8 = 1,
 s_0_7 = 0,
 s_0_6 = 0,
 s_0_5 = 0,
 s_0_4 = 0,
 s_0_3 = 0,
 s_0_2 = 0,
 s_0_1 = 0]

見やすくするためクイーンの存在するところにX, 存在しないところに.を表示してみよう solverのmodel() で得られのは辞書 (dictionary)で，変数をキーとして割り当て結果が得られるが， 整数型の変数の場合は，IntNumRefなので，普通の整数にするにはas_long() で変換する必要がある．

In [12]:
m = solver.model()
for r in squares:
    print(''.join('X' if m[r[i]].as_long()  == 1 else '.' for i in range(n)))

........X.
...X......
X.........
....X.....
.......X..
.........X
......X...
..X.......
.....X....
.X........
In [ ]: