Z3の使い方 ― 5つのステップで制約を解く

Z3の使い方 ― 5つのステップで制約を解く#

この章で学ぶこと#

前の章では、Z3 を使うと制約充足問題を短く書けることを見ました。この章では、Z3 の使い方を基本の流れから順番に確認します。

  • Z3 で問題を解く5つのステップ

  • Z3 の変数が、普通の Python の数とどう違うか

  • モデル（答え）から値を取り出す方法

  • 例題「SEND + MORE = MONEY」を解く

  • 解をすべて列挙する方法

この章のコードは上から順に実行してください。前のコードで作った変数を、次のコードで使っています。

from z3 import *

Z3で解く流れ#

Z3 で問題を解く手順は、どんな問題でもほとんど同じです。

ステップ

やること

使うもの

1

変数を作る

Int, Ints, IntVector

2

ソルバーを用意する

Solver()

3

制約を追加する

solver.add()

4

解があるか調べる

solver.check()

5

値を取り出す

solver.model()

この5つを、順番に見ていきます。

ステップ1：変数を作る#

まず、値がまだ決まっていない変数を作ります。作り方は3通りあります。

x = Int("x")             # 整数変数を1つ作る
y, z = Ints("y z")       # 名前を空白で区切って、まとめて作る
v = IntVector("v", 5)    # v[0] 〜 v[4] の5つの整数変数

作った変数の型は ArithRef です。IntVector は Python のリストで、中身が ArithRef になっています。

print(type(x), x, y, z)
print(type(v), type(v[0]), v)

<class 'z3.z3.ArithRef'> x y z
<class 'list'> <class 'z3.z3.ArithRef'> [v__0, v__1, v__2, v__3, v__4]

Z3 の変数は、普通の Python の数とは動きが違います。値がまだ決まっていないので、計算しても数値にならず、式のまま残ります。

print(x + 1)            # 計算されず、式のまま表示される
print(x + 1 == 10)      # 条件式（BoolRef）になる
print(type(x + 1 == 10))

x + 1
x + 1 == 10
<class 'z3.z3.BoolRef'>

ステップ2：ソルバーを用意する#

制約を溜めておいて、解を探してくれるのが Solver です。まず空のソルバーを作ります。

solver = Solver()
print(type(solver), solver)   # [] は「まだ制約がない」という意味

<class 'z3.z3.Solver'> []

ステップ3：制約を追加する#

solver.add() に制約を渡します。==, <, >, + などの演算子が、そのまま制約の式になります。

制約は1つずつ渡しても、リストにまとめて渡してもかまいません。

solver = Solver()

constraints = [
    x + y == 10,   # x と y の合計は 10
    x > 0,         # x は正の数
    y > 0,         # y は正の数
]
solver.add(*constraints)   # リストを展開して渡す（solver.add(a, b, c) と同じ）
print(solver)

[x + y == 10, x > 0, y > 0]

solver を print() すると、今入っている制約がすべて表示されます。思ったとおりの条件が入ったか確認するのに便利です。

ステップ4：解があるか調べる#

Solver.check() で、制約を満たす解があるかどうかを調べます。返ってくる答えは3種類です。

戻り値

意味

sat

解が見つかった（satisfiable）

unsat

解は存在しない（unsatisfiable）

unknown

判断できなかった（時間切れ、Z3 が苦手な式が混ざっている など）

 
if solver.check() == sat:
    print("解あり")
else:
    print("解なし")

解あり

ステップ5：モデルから値を取り出す#

解があるときは、solver.model() で具体的な値を取り出せます。返ってくるのは ModelRef というオブジェクトです。

if solver.check() == sat:
    model = solver.model()
    print("x =", model[x])
    print("y =", model[y])
else:
    print("解なし")

x = 9
y = 1

model[x] は Z3 の IntNumRef 型で、そのままでは Python の整数として計算できません。as_long() で変換します。

print(type(model), type(model[x]))

print("x =", model[x].as_long())
print("x + y =", model[x].as_long() + model[y].as_long())

<class 'z3.z3.ModelRef'> <class 'z3.z3.IntNumRef'>
x = 9
x + y = 10

例題：SEND + MORE = MONEY#

OrTools で同じ問題を解く

文字を数字に置き換えるパズル（覆面算、Cryptarithm）です。

S, E, N, D, M, O, R, Y は、それぞれ 0〜9 の違う数字を表します。

\[SEND + MORE = MONEY\]

この式が成り立つ数字の組み合わせを求めてください。

答えは \(9567 + 1085 = 10652\) です。Z3 で本当にその答えが出るか、確かめてみましょう。

解き方は、この章の5ステップそのままです。

  1. S, E, N, D, M, O, R, Y を整数変数にする

  2. どの文字も 0〜9、しかもすべて違う値、という制約を追加する

  3. 単語を数式にする：\(SEND = 1000S + 100E + 10N + D\)

  4. \(SEND + MORE = MONEY\) を制約として追加する

  5. check() と model() で解を取り出す

# S, E, N, D, M, O, R, Y を整数変数にする
S, E, N, D, M, O, R, Y = Ints("S E N D M O R Y")
letters = [S, E, N, D, M, O, R, Y]

solver = Solver()

# 1. どの文字も 0〜9 のどれか
for letter in letters:
    solver.add(0 <= letter, letter <= 9)

# 2. 文字が違えば、数字も違う
solver.add(Distinct(letters))

# 3. 単語を数式にする  例：SEND = 1000*S + 100*E + 10*N + D
send = 1000*S + 100*E + 10*N + D
more = 1000*M + 100*O + 10*R + E
money = 10000*M + 1000*O + 100*N + 10*E + Y

# 4. SEND + MORE = MONEY
solver.add(send + more == money)

# 5. 先頭の桁に 0 は入らない
solver.add(S != 0, M != 0)

if solver.check() == sat:
    model = solver.model()
    print({str(letter): model[letter].as_long() for letter in letters})
    print(f"{model.eval(send)} + {model.eval(more)} = {model.eval(money)}")
else:
    print("解なし")

{'S': 9, 'E': 5, 'N': 6, 'D': 7, 'M': 1, 'O': 0, 'R': 8, 'Y': 2}
9567 + 1085 = 10652

答えは1通りだけでした。コードで使った演算子は2つだけです。

演算子

役割

例

And

すべての条件を満たす

And(x > 0, y > 0)

Distinct

与えた変数がすべて違う値になる

Distinct(a, b, c)

値の取り出し方も2通りあります。

  • model[x] … 変数の値を取り出す

  • model.eval(式) … 式の計算結果を取り出す

モデルの中身#

ModelRef は、変数と値をまとめたものです。[] に何を渡すかで、返ってくるものが変わります。

渡すもの

返ってくるもの

変数（ArithRef）

その値（IntNumRef）

添字（整数）

変数の宣言（FuncDeclRef）

 
print(model[0], type(model[0]))   # 0番目の変数の「宣言」

decl = model[0]
print(decl(), type(decl()))       # () を付けると変数（ArithRef）になる

S <class 'z3.z3.FuncDeclRef'>
S <class 'z3.z3.ArithRef'>

FuncDeclRef は変数の宣言なので、() を付けると変数そのものになります。どの文字が0番目になるかは Z3 の内部の順番で決まるため、実行するたびに変わるかもしれません。

この仕組みを使うと、モデルに入っているすべての変数の値を一度に取り出せます。

{str(decl): model[decl].as_long() for decl in model}

{'S': 9, 'O': 0, 'N': 6, 'R': 8, 'E': 5, 'M': 1, 'Y': 2, 'D': 7}

すべての解を列挙する#

「解を1つ」ではなく「すべての解」が欲しいときは、見つけた解をもう出さないという制約を追加して、check() を繰り返します。

  1. check() で解があるか調べる

  2. model() で解を取り出す

  3. 「この解はもう出さない」という制約を追加して、1に戻る

  4. 解がなくなったら（unsat）終了

abc = Ints("a b c")
solver = Solver()

for n in abc:
    solver.add(1 <= n, n <= 3)   # どれも 1〜3 のどれか
solver.add(Distinct(abc))        # 3つとも違う値

while solver.check() == sat:
    model = solver.model()
    print(model)
    # 今見つけた解と「すべて同じ」になる組み合わせを禁止する
    solver.add(Not(And([decl() == model[decl] for decl in model])))

[c = 2, b = 3, a = 1]
[a = 3, c = 1, b = 2]
[c = 2, b = 1, a = 3]
[c = 1, b = 3, a = 2]
[c = 3, a = 2, b = 1]
[a = 1, c = 3, b = 2]

Not(And(c1, c2, ...)) は Or(Not(c1), Not(c2), ...) と同じ意味です。つまり「どれか1つでも違えばよい」＝「前と同じ解ではない」という制約になります。

次の1行でも同じことができます。

solver.add(Or([decl() != model[decl] for decl in model]))

ただし、この方法は解の数だけ check() を呼びます。解がたくさんある問題では時間がかかるので、注意してください。

まとめ#

Z3 で問題を解く流れは、いつも同じ5ステップです。

  1. 変数を作る（Int, Ints, IntVector）

  2. Solver() を作る

  3. solver.add() で制約を追加する

  4. solver.check() で sat / unsat / unknown を確認する

  5. solver.model() で値を取り出し、as_long() で Python の整数にする

  • Z3 の変数は「まだ決まっていない値」で、式计算のまま扱う

  • print(solver) で制約を確認すると、書き間違いに気づきやすい

  • すべての解が欲しいときは、見つけた解を禁止する制約を足して繰り返す