Z3Py 例題 エイト・クイーン問題

問題

8×8 のボード上に，8つのチェスのクイーンのコマを置く．
8つのクイーンが互いに取られないように配置することはできるか?
(エイト・クイーン)

回答

example_8_Queen.py

from z3 import *

X = [[Int("x_%s_%s" % (i, j)) for j in range(8)]for i in range(8)]

s = Solver()
s.add([And(0 <= X[i][j], X[i][j] <= 1) for i in range(8) for j in range(8)])
s.add([Sum([X[i][j]for i in range(8)]) == 1 for j in range(8)])
s.add([Sum([X[i][j]for j in range(8)]) == 1 for i in range(8)])
for a in range(-6, 7):
    diag = []
    for i in range(8):
        if (0 <= i+a) & (i+a <= 7):
            diag.append(X[i+a][i])
    s.add(Sum(diag) <= 1)

for a in range(-6, 7):
    diag = []
    for i in range(8):
        if (0 <= i+a) & (i+a <= 7):
            diag.append(X[i+a][7-i])
    s.add(Sum(diag) <= 1)

print(s.check())
m = s.model()
for i in range(8):
    tmp = []
    for j in range(8):
        tmp.append(m[X[i][j]])
    print(tmp)

出力

sat
[0, 0, 0, 0, 0, 1, 0, 0]
[0, 0, 0, 1, 0, 0, 0, 0]
[0, 1, 0, 0, 0, 0, 0, 0]
[0, 0, 0, 0, 0, 0, 0, 1]
[0, 0, 0, 0, 1, 0, 0, 0]
[0, 0, 0, 0, 0, 0, 1, 0]
[1, 0, 0, 0, 0, 0, 0, 0]
[0, 0, 1, 0, 0, 0, 0, 0]

解説

他の例題

Z3Py個人的ポータル へ