Z3の基本

Z3の基本#

from z3 import *

流れ#

Z3で問題を解く一般的な流れを、詳細に説明します。

  1. 変数を作成する

Z3では、整数変数 (Int や Ints)、整数配列 (IntVector) などを使って変数を作成します。

  • Int("x") のように変数を1つずつ作成

  • Ints("x y z") のように複数変数を一括作成

  • IntVector("v", 5) のようにベクトルを作成

x = Int("x")  # 変数 x を作成
y, z = Ints("y z")  # 複数の変数を作成
v = IntVector("v", 5)  # v[0] 〜 v[4] の整数変数ベクトル

作った整数変数はの型は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]

  1. Solver を作成する

制約を追加し、解を求めるために Solver() オブジェクトを作成します。

solver = Solver()
print(type(solver), solver)

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

  1. 制約条件を追加する

solver.add() を使って制約条件を追加します。+, >, <, == のような演算子を使って制約条件を作成できます。

solver.add(x + y == 10)  # x + y = 10
solver.add(x > 0, y > 0)  # x, y は正の整数

また、リストを使って一括で追加することもできます。Solver オブジェクトを print() で出力すると、含まれているすべての制約条件が表示されます。

constraints = [
    x + y == 10,
    x > 0,
    y > 0
]
solver.add(*constraints)
print(solver)

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

  1. 制約を満たす解があるか確認する

solver.check() を使って、制約を満たす解が存在するかどうかをチェックします。以下の三種類の結果が得られる可能性があります。

  • sat: 解が存在する

  • unsat: 解が存在しない

  • unknown: 計算不能（時間制限や不完全な理論）

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

解あり

  1. モデルを取得して解を表示

制約を満たす具体的な解を取得するには、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で、直接整数として扱うことができません。

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

<class 'z3.z3.ModelRef'> <class 'z3.z3.IntNumRef'>

as_long()メソッドでPythonの整数型に変換します。

model[x].as_long()

9

「SEND + MORE = MONEY」を解く#

OrToolsでSEND+MORE=MONEYを解く

この問題は「文字を数字に置き換えるパズル」（Cryptarithm）の一種です。

それぞれのアルファベット（S, E, N, D, M, O, R, Y）は0〜9の異なる数字を表し、次の計算が成り立つように求めます。

\[SEND + MORE = MONEY\]

例えば、もし

  • S = 9, E = 5, N = 6, D = 7

  • M = 1, O = 0, R = 8, Y = 2

だった場合、次のような計算になります。

\[ 9567 + 1085 = 10652 \]

Z3で解く流れは以下のようになります。

  1. 変数を作成

    • 各文字（S, E, N, D, M, O, R, Y）を整数変数として定義

    • 0〜9の範囲で、すべて異なる値を取る制約を追加

  2. 制約を追加

    • \( SEND = 1000S + 100E + 10N + D \)

    • \( MORE = 1000M + 100O + 10R + E \)

    • \( MONEY = 10000M + 1000O + 100N + 10E + Y \)

    • それらが \( SEND + MORE = MONEY \) を満たすようにする

    • S と M は 0 ではない（最上位の桁に 0 は入らない）

  3. Z3で解を求める

    • solver.check() で解が存在するか確認

    • solver.model() で解を取得

# 変数定義
S, E, N, D, M, O, R, Y = Ints("S E N D M O R Y")

# Solver 作成
solver = Solver()

# 各変数は 0 〜 9 の整数
vars = [S, E, N, D, M, O, R, Y]
solver.add([And(v >= 0, v <= 9) for v in vars])

# すべての変数は異なる
solver.add(Distinct(vars))

# 4桁の数字を式に変換
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

# 制約条件追加
solver.add(SEND + MORE == MONEY)

# S と M は 0 ではない（最上位の桁なので）
solver.add(S > 0, M > 0)

# 解を求める
if solver.check() == sat:
    model = solver.model()
    solution = {str(v): model[v].as_long() for v in model}
    print("解:", solution)
    print(f"{model.eval(SEND)} + {model.eval(MORE)} = {model.eval(MONEY)}")
else:
    print("解なし")

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

ModelRef オブジェクトから解を取得するとき、変数の場合は [] を使って値を取得できます。変数や演算式の場合は eval() メソッドを使用して値を取得できます。

上のコードでは次の二つ演算子を使っています。

  • And は複数の条件をすべて満たす必要がある場合に使用します。 これは論理的なAND演算を表します。

  • Distinct は、与えられた変数がすべて異なる値を取るようにするために使います。

演算子

役割

例

And

すべての条件を満たす

And(x > 0, y > 0)

Distinct

すべての変数が異なる値を取る

Distinct(a, b, c)

ModelRef オブジェクトのインデックス操作：

  • インデックスが整数の場合: FuncDeclRef 型の変数を取得します。

  • インデックスが FuncDeclRef 型の場合: 値を表す IntNumRef 型のオブジェクトを取得します。

v = model[0]
n = model[v]
print(type(v), v)
print(type(n), n)

<class 'z3.z3.FuncDeclRef'> R
<class 'z3.z3.IntNumRef'> 8

この性質を利用すると、ModelRef オブジェクトだけで、すべての変数の値を取得できます。

{str(v): model[v] for v in model}

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

値を Python のデータ型に変換する場合は、as_long() などのメソッドを使用します。

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

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

FuncDeclRef 型のオブジェクトを実行すると、Int() で作成された ArithRef 型のオブジェクトを取得します。

print(type(v()), v())

<class 'z3.z3.ArithRef'> R

全ての解を取得#

全ての解を取得するには、現在得られた解を除外する制約を追加し、check() を繰り返す方法を用います。以下に、すべての解を列挙する手順を示します。

  1. solver.check() を実行し、解があるかを確認します。解があればステップ 2 へ、なければ終了します。

  2. solver.model() で解を取得します。

  3. 取得した解を除外する制約を追加し、ステップ 1 に戻ります。

xs = Ints('a b c')
solver = Solver()
for v in xs:
  solver.add(1 <= v, v <= 3)
solver.add(Distinct(xs))

while solver.check() == sat:
    model = solver.model()
    print(model)
    solver.add(Not(And([v() == model[v] for v in model]))) #modelの解を除外する

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

Not(And(cond1, cond2, ...)) は Or(Not(cond1), Not(cond2), ...) に変換できるため、次のコードでも同じ動作を実現できます。

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