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)
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()の詳細
他の例題
Author And Source
この問題について(Z3Py 例題 魔方陣（magic square）), 我々は、より多くの情報をここで見つけました https://qiita.com/Ganesha/items/fdf965e75f1a49004dd8著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。
Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .