n-queenを解く(bool版)

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 のマス square[y][x] にqueenが置かれている時にTrue, 置かれていない時にFalseになるようにしたい．

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

制約を書く

まず行の中にTrueとなっているものがあることを書く

次に各行のいずれかの要素がTrueになっていること，各行の中にTrueが複数回現れないことを書く．

In [4]:
for r in squares:
    solver.add(Or(r))
    for i in range(1, n, 1):
        for j in range(i):
            solver.add(Or(Not(r[i]),Not(r[j])))
In [5]:
In [11]:
次に各列のいずれかの要素がTrueになっているという制約，同時に2つがTrueになることはないを書く．
In [5]:
for x in range(n):
    solver.add(Or([r[x] for r in squares]))
    for i in range(1, n, 1):
        for j in range(i):
            solver.add(Or(Not(squares[i][x]),Not(squares[j][x])))

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

In [6]:
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(Or(Not(squares[y0][x0]), Not(squares[y1][x1])))

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

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

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

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

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

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

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