Python+Z3で魔方陣
魔方陣をPythonで自動的に作るとなると全パターンを挙げて埋めていけば理論上はできるのですが、時間がかかりすぎます。
Z3を使って作ってみました。
3*3
from z3 import *
# 変数の作成
a, b, c, d, e, f, g, h, i = Ints(["a", "b", "c", "d", "e", "f", "g", "h", "i"])
# ソルバのインスタンスを生成
slv = Solver()
# 制約 異なる値を持つ
slv.add(Distinct([a, b, c, d, e, f, g, h, i]))
# 制約 1以上9以下
slv.add(0 < a, a < 10)
slv.add(0 < b, b < 10)
slv.add(0 < c, c < 10)
slv.add(0 < d, d < 10)
slv.add(0 < e, e < 10)
slv.add(0 < f, f < 10)
slv.add(0 < g, g < 10)
slv.add(0 < h, h < 10)
slv.add(0 < i, i < 10)
# 制約 計算
slv.add(a + b + c == 15)
slv.add(d + e + f == 15)
slv.add(g + h + i == 15)
slv.add(a + d + g == 15)
slv.add(b + e + h == 15)
slv.add(c + f + i == 15)
slv.add(a + e + i == 15)
slv.add(c + e + g == 15)
# メイン
result = slv.check()
if result == sat:
mdl = slv.model()
print(mdl[a], mdl[b], mdl[c])
print(mdl[d], mdl[e], mdl[f])
print(mdl[g], mdl[h], mdl[i])
else:
print(result)
# 変数の作成
a, b, c, d, e, f, g, h, i = Ints(["a", "b", "c", "d", "e", "f", "g", "h", "i"])
# ソルバのインスタンスを生成
slv = Solver()
# 制約 異なる値を持つ
slv.add(Distinct([a, b, c, d, e, f, g, h, i]))
# 制約 1以上9以下
slv.add(0 < a, a < 10)
slv.add(0 < b, b < 10)
slv.add(0 < c, c < 10)
slv.add(0 < d, d < 10)
slv.add(0 < e, e < 10)
slv.add(0 < f, f < 10)
slv.add(0 < g, g < 10)
slv.add(0 < h, h < 10)
slv.add(0 < i, i < 10)
# 制約 計算
slv.add(a + b + c == 15)
slv.add(d + e + f == 15)
slv.add(g + h + i == 15)
slv.add(a + d + g == 15)
slv.add(b + e + h == 15)
slv.add(c + f + i == 15)
slv.add(a + e + i == 15)
slv.add(c + e + g == 15)
# メイン
result = slv.check()
if result == sat:
mdl = slv.model()
print(mdl[a], mdl[b], mdl[c])
print(mdl[d], mdl[e], mdl[f])
print(mdl[g], mdl[h], mdl[i])
else:
print(result)
実行結果
2 7 6
9 5 1
4 3 8
4*4
from z3 import *
# 変数の作成
ax = []
ax = Ints([f"ax{x}" for x in range(0, 16)])
# ソルバのインスタンスを生成
slv = Solver()
# 制約 異なる値を持つ
slv.add(Distinct(ax))
# 制約 範囲
for i in range(0, 16):
slv.add(0 < ax[i], ax[i] < 17)
# 成約 計算
for i in range(0, 4):
slv.add(ax[i * 4] + ax[i * 4 + 1] + ax[i * 4 + 2] + ax[i * 4 + 3] == 34)
slv.add(ax[i] + ax[i + 4] + ax[i + 8] + ax[i + 12] == 34)
slv.add(ax[0] + ax[5] + ax[10] + ax[15] == 34)
slv.add(ax[3] + ax[6] + ax[9] + ax[12] == 34)
result = slv.check()
if result == sat:
mdl = slv.model()
# print(mdl)
for i in range(0, 4):
for j in range(0, 4):
print(mdl[ax[i * 4 + j]], end = " ")
print()
else:
print(result)
# 変数の作成
ax = []
ax = Ints([f"ax{x}" for x in range(0, 16)])
# ソルバのインスタンスを生成
slv = Solver()
# 制約 異なる値を持つ
slv.add(Distinct(ax))
# 制約 範囲
for i in range(0, 16):
slv.add(0 < ax[i], ax[i] < 17)
# 成約 計算
for i in range(0, 4):
slv.add(ax[i * 4] + ax[i * 4 + 1] + ax[i * 4 + 2] + ax[i * 4 + 3] == 34)
slv.add(ax[i] + ax[i + 4] + ax[i + 8] + ax[i + 12] == 34)
slv.add(ax[0] + ax[5] + ax[10] + ax[15] == 34)
slv.add(ax[3] + ax[6] + ax[9] + ax[12] == 34)
result = slv.check()
if result == sat:
mdl = slv.model()
# print(mdl)
for i in range(0, 4):
for j in range(0, 4):
print(mdl[ax[i * 4 + j]], end = " ")
print()
else:
print(result)
実行結果
14 9 8 3
15 2 11 6
1 16 5 12
4 7 10 13
[ 2024年2月18日 | カテゴリー: Python | タグ: Z3 , 魔方陣 ]
« AIが選ぶ日本の歌姫 | ガストの価格は3種類 »
コメントを残す