Z3Py 例題 魔方陣（magic square）

問題

1から9の数字を 3×3 に配置し、各行・各列・各対角線の和がいずれも15になるようにせよ。（魔方陣）

回答

example03_magic_square.py

from z3 import *

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

s = Solver()
s.add([And(1 <= X[i][j], X[i][j] <= 9) for i in range(3) for j in range(3)])
s.add([Distinct([X[i][j] for i in range(3) for j in range(3)])])
s.add([Sum([X[i][j] for i in range(3)]) == 15 for j in range(3)])
s.add([Sum([X[i][j] for j in range(3)]) == 15 for i in range(3)])
s.add([Sum([X[i][i] for i in range(3)]) == 15])
s.add([Sum([X[i][2-i] for i in range(3)]) == 15])

print(s.check())

m = s.model()
for i in range(3):
    row = []
    for j in range(3):
        row.append(m[X[i][j]])
    print(row)

出力

sat
[6, 7, 2]
[1, 5, 9]
[8, 3, 4]

解説

Distinct()は、「入力した変数群は互いに異なる」という制約を生成します。
例）Distinct(x, y, z)　→　And(Not(x == y), Not(x == z), Not(y == z))
Distinct()の詳細

他の例題

Z3Py個人的ポータル へ