z3を使ってパズルを解く

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

n-queens を解く

n-queens は

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

In [1]:
from z3 import *

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

準備

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

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

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

変数を作る

解くパズルは「変数」と「制約」で表現する． 「変数」としては，bool変数，整数変数などいろいろある．n-queensを表現する方法はいろいろあるが，まずは， n x n のy行目の何マス目にqueenが置かれているかを表す配列 rows[y] を作る．

In [4]:
rows = [Int('r_%d' % y) for y in range(n)]

制約を書く

まずrowsの要素は0以上n未満である．それを書く

In [5]:
for r in rows:
    solver.add(0 <= r, r < n)

次にrowsの中に重複要素がないこと，斜め同士の関係にないことを書く．

In [6]:
for i in range(n):
    for j in range(i):
        solver.add(rows[i] != rows[j], rows[i] - rows[j] != i - j, rows[j] - rows[i] != i - j)

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

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

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

In [8]:
solver.model()
Out[8]:
[r_0 = 1,
 r_4 = 2,
 r_7 = 3,
 r_6 = 6,
 r_5 = 9,
 r_1 = 8,
 r_2 = 5,
 r_3 = 0,
 r_8 = 7,
 r_9 = 4]

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

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

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