Ctrl+K

課題: SMTによる解の探索

Contents

課題: SMTによる解の探索#

See also

!pip install -U z3-solver

Collecting z3-solver
  Using cached z3_solver-4.13.0.0-py2.py3-none-manylinux2014_x86_64.whl.metadata (757 bytes)
Using cached z3_solver-4.13.0.0-py2.py3-none-manylinux2014_x86_64.whl (57.3 MB)
Installing collected packages: z3-solver
Successfully installed z3-solver-4.13.0.0

from z3 import *

# 変数定義
x = Int("x")
y = Int("y")

# 基本制約
s = Solver()
s.add(x > 0, y > 0)
s.add(x + y < 5)

# 解を探索
while(s.check() == sat):
    # 解の表示
    m = s.model()
    print(m)

    # 解を制約条件に追加
    s.add(Not(And(x == m[x], y == m[y])))

[x = 1, y = 1]
[x = 2, y = 2]
[x = 3, y = 1]
[x = 2, y = 1]
[x = 1, y = 3]
[x = 1, y = 2]

3×3の魔方陣#

from z3 import *
import sys

n = 3

x = [[Int("x[%d,%d]" % (i,j)) for j in range(n)] for i in range(n)]
s = Solver()

for i in range(n):
    for j in range(n):
        s.add(1 <= x[i][j], x[i][j] <= n*n)

# all numbers are unique
s.add(Distinct(sum(x, [])))

# all rows have same sum
for i in range(1, n):
    s.add(sum(x[0]) == sum(x[i]))

# all columns have same sum
for j in range(1, n):
    s.add(sum(map(lambda row: row[0], x)) == sum(map(lambda row: row[j], x)))

s.check()
m = s.model()

for i in range(n):
    for j in range(n):
        sys.stdout.write(" %2d" % m[ x[i][j] ].as_long())
    sys.stdout.write("\n")

  6  7  2
  8  3  4
  1  5  9

print(s.assertions())

[x[0,0] >= 1,
 x[0,0] <= 9,
 x[0,1] >= 1,
 x[0,1] <= 9,
 x[0,2] >= 1,
 x[0,2] <= 9,
 x[1,0] >= 1,
 x[1,0] <= 9,
 x[1,1] >= 1,
 x[1,1] <= 9,
 x[1,2] >= 1,
 x[1,2] <= 9,
 x[2,0] >= 1,
 x[2,0] <= 9,
 x[2,1] >= 1,
 x[2,1] <= 9,
 x[2,2] >= 1,
 x[2,2] <= 9,
 Distinct(x[0,0],
          x[0,1],
          x[0,2],
          x[1,0],
          x[1,1],
          x[1,2],
          x[2,0],
          x[2,1],
          x[2,2]),
 0 + x[0,0] + x[0,1] + x[0,2] ==
 0 + x[1,0] + x[1,1] + x[1,2],
 0 + x[0,0] + x[0,1] + x[0,2] ==
 0 + x[2,0] + x[2,1] + x[2,2],
 0 + x[0,0] + x[1,0] + x[2,0] ==
 0 + x[0,1] + x[1,1] + x[2,1],
 0 + x[0,0] + x[1,0] + x[2,0] ==
 0 + x[0,2] + x[1,2] + x[2,2]]
Contents