まずは，z3というモジュールに含まれる定義を使うことを宣言する．

In [1]:
from z3 import *

solverを作る

In [3]:
solver = Solver()

実数型の変数を作る．それぞれが非負であるという制約をsolverに加える．

In [6]:
x = Real("x")
y = Real("y")
solver.add(x >= 0)
solver.add(y >= 0)

制約式p1, p2, p3 を作り，それを元に作成した節を加える．

In [7]:
p1 = (x + y <= 2)
p2 = (2 * x + y <= 3)
p3 = (x + y >= 3)
solver.add(p3)
solver.add(Or(p1, p2))
solver.add(Or(Not(p1), Not(p2)))

制約を満たす変数割り当てがあるかどうかをチェックする．

In [9]:
solver.check()
Out[9]:
sat
In [ ]:
変数割り当ての一つを表示させる．
In [10]:
solver.model()
Out[10]:
[y = 3, x = 0]

別解があるかどうかを調べるために，見つかった解を除く制約を加える

In [11]:
solver.add(Or(y != 3, x != 0))

制約を満たす変数割り当てがあるかどうかをチェックする．

In [12]:
solver.check()
Out[12]:
unsat

なお，solveという関数で一度に解くこともできる．

In [14]:
x, y = Reals("x y")
p1 = (x + y <= 2)
p2 = (2 * x + y <= 3)
p3 = (x + y >= 3)
solve(x >= 0, y >= 0, p3, Or(p1, p2), Or(Not(p1), Not(p2)))

[y = 3, x = 0]
In [ ]: