『Logic for Programmers』を執筆する過程で、大量の「カス」が生まれました。書き上げたものの結局ボツにしたコードサンプルや節のことです。同じトピックでもっと良い例が見つかったこともあれば、トピック自体を丸ごと捨てたこともあります。せっかく書いたものをハードディスクの中で腐らせるのはもったいないので、その中から「Z3」というツールを扱ったカスの束を共有することにしました。Z3はソフトウェア研究のさまざまな場面で使われています。

まずはこのツールがそもそも何なのかを説明し、そのあと面白さが徐々に増していく順番でスクリプトを紹介します。すべての例ではPythonバインディング（pip install z3-solver）を使います。

Z3とは？

Z3はSMTソルバーです。

なるほど、ではSMTとは？

SMT（“Satisfiability Modulo Theories”）ソルバーとは、数学やプログラミングの基本的な概念を理解する制約ソルバーです。いくつかの変数と、それらを使った等式を与えると、すべての等式を満たす割り当ての集合、すなわちモデルを見つけようとしてくれます。

12歳になって初めて代数Iの授業を受けている場面を想像してみてください。こんな問題が出てきました。

4x + 2y == 14
2x - y  == 1
solve for x & y

本来なら連立方程式として解く方法を学ぶところですが、勉強する機会を自らドブに捨てたいなら、Z3に解かせることもできます。

# pip install z3-solver
import z3

s = z3.Solver()
x, y = z3.Ints('x y')

s.add(4*x + 2*y == 14)
s.add(2*x - y  == 1)

result = s.check()
print(result)
if result == z3.sat:
    print(s.model())

これがZ3のもっとも一般的な使い方です。ソルバーを生成し、制約を追加して、チェックします。¹ Ints('x y')は2つの「定数」を作ります。s.check()を呼び出すと、ソルバーはすべての制約を満たす定数の値（モデル）を探します。ここでは「sat」に続けて[x = 2, y = 3]と表示されます。複数の解がある場合は最初に見つかったものが返り、解がなければ「unsat」と表示されます。

これが「充足可能性（satisfiability）」の部分です。「Modulo Theories」の部分は、Z3が異なる領域、つまり「理論」ごとに特化したソルバーを多数抱えていることに由来します。そのおかげで、配列や正規表現、量化式などを含む制約も扱えるのです。

ここからはイケてる人たちにならって、Z3のAPI全体を名前空間にインポートすることにします。

スクリプト集

ふと浮かんだおバカな数学の疑問

互いに異なる4つの正の整数a, b, c, dで、a + b = c + dかつa * b = c * dを満たすものは存在するだろうか？

すべての制約を最も素直に表現すると、こうなります。

from z3 import *
s = Solver()

a, b, c, d = Ints('a b c d')
s.add(a > 0, b > 0, c > 0, d > 0)
s.add(a + b == c + d)
s.add(a * b == c * d)

# We can add many constraints in one `add` call
s.add(a != b, a != c, a != d, 
      b != c, b != d, c != d)

print(s.check())

これは「unsat」を返します。つまり、そのようなペアは存在しないということです。振り返ってみれば当然だったはずです。証明はドロップダウンをご覧ください。

では、異なる2つのトリプル、つまり6つの異なる数で同じことを試したらどうなるでしょう？15個もの不等号を書くのはごめんなので、少しシンタックスシュガーを導入しましょう。

• IntVector('lhs', 3)は変数のリスト[lhs__0, lhs__1, lhs__2]を返します。
• SumとProductは見たままの動きをします。²
• Distinct(l)はlの中のすべての値が互いに異ならなければならないことを表します。

これらを使えば、スクリプトをもっとスケーラブルにできます。

from z3 import *
n = 3
lhs = IntVector("lhs", n)
rhs = IntVector("rhs", n)

s = Solver()
for x in lhs + rhs: 
    s.add(x >= 0) 
s.add(sum(lhs) == sum(rhs))
s.add(Product(lhs) == Product(rhs))
s.add(Distinct(lhs + rhs))

if s.check() == sat:
    m = s.model()
    l = [m[l].as_long() for l in lhs]
    r = [m[r].as_long() for r in rhs]
    print(l, r)
    print(f"sum={sum(l)} prod={Product(l)}")
else:
    print("unsat")

今度はトリプルのペアが見つかります。[7, 8, 15]と[14, 6, 10]は和が30、積が840で一致します。

これを実行すると別の例が得られるかもしれません。なぜなら、単に「どれでもいいから満たすモデル」を求めているだけだからです。新しい制約を追加すれば別のモデルを見つけられますし、ソルバーをオプティマイザーに変えて、見つかった和や積を最小化することもできます。

- s = Solver()
+ s = Optimize()
+ s.minimize(Sum(lhs))

これは[8, 2, 9]と[4, 12, 3]を返します。和は19、積は144です。

毎年の積立額を最小化する

Z3のオプティマイザーはMiniZincのような専用の制約ソルバーと比べるとかなり時間がかかりますが、それでも簡単な問題なら解くことができます。

ある銀行口座は年利1%です。20年後に10,000ドル貯めるには、毎年最低いくら預ければよいでしょう？預入は利息が支払われた後に行われるものとします。

つまり1年目はCドル、2年目はC*1.01 + Cドル、という具合です。SMTでは定数の値を再代入することはできませんが、ここでPythonの抽象化が少し漏れ出します。例えばこう書いたとします。

x = Int('foo')
x = x + x
s.add(x < 6)

一見、Python変数xにSMT定数fooを代入しているように見えますが、実際にはxには「fooの値」という式が代入されています。x = x + xという行は、xに「fooの値＋fooの値」という式を代入し、その次の行はfoo + foo < 6という制約を追加することになります。

ということは、次のように利息を複利で計算できます。

years = 20
goal = 10000

r = RealVal('1.01')
c = Real('c')
balance = c

for t in range(1, years):
    balance = balance*r+c

今回はIntではなくRealを使っています。Realはざっくり言えば無限精度の浮動小数点のようなものです。³ rはRealValである必要があります。なぜならこれは固定値であって、Z3が解くべき対象ではないからです。これで20年後のbalanceの最終的な値が計算されます。

とはいえ、この方法では14年目のbalanceがいくつなのかを知ることができません。途中の結果も知りたい場合は、balanceを20個のRealの配列にして、balance[0]を初期値、balance[n] == balance[n-1]*r + cとします。全体のモデルは次のとおりです。

from z3 import * # type: ignore

years = 20
goal = 10000

r = RealVal('1.01')
balance = RealVector('balance', years)
c = Real('c')

opt = Optimize()
opt.minimize(c)

opt.add(balance[0] == c)
for t in range(1, years):
    opt.add(balance[t] == balance[t-1] * r + c)

if opt.check(balance[years-1] >= goal) == sat:
    m = opt.model()
    print(f"c = {m[c].as_decimal(2)}")
    for x, i in enumerate(balance):
        print(f"balance[{x}] = {m[i].as_decimal(2)}")
else:
    print("unsat")

これで最適な預入額はC=453.4だとわかります。Z3での最適化はとにかく遅いのであまり人気のある使い方ではありませんが、それでもかなりクールな機能です。⁴

これは便利な小技も示しています。check()に追加の制約を渡して呼び出せるのです。私も比較的最近までこれが可能だと知りませんでした！同じ問題の多くのインスタンスを解きたい場合に便利そうですが、私が見た限りでは、人々は1つのソルバーを新しい制約で「パラメータ化」するよりも、その都度新しいソルバーオブジェクトを生成する方を好むようです。

RNGのリバースエンジニアリング

本を書くにあたって私がぜひやりたかったことの一つは、紹介する各トピックに実用的な応用例を付けることです。すべてのプログラマーに刺さる必要はありません。「これを学べば世の中の誰かの役に立ちそうだ」と思える程度に有用であれば十分です。そこでRNGの値をリバースエンジニアリングする例を書くことにしました。

ソフトウェアにおけるほとんどの乱数生成器は、実際には擬似乱数です。決定的な数学的アルゴリズムを使って、多くの用途では「十分にランダムな」数の列を生成します。このことについてはこちらで詳しく話しています。そのようなアルゴリズムの一つが線形合同法（LCG）です。LCGには固定の定数（a、c、m）と開始シードであるXがあり、次の値は次のように計算されます。

X = (a * X + c) % m

例えばa = 6, m = 59, c = 0なら、1から始まる数列は1, 6, 36, 39, 57…と続きます。とはいえ、たいていの数列ではもっと大きな値が使われます。数列とmを受け取って(a, c)を再計算するSMT問題を書いてみましょう。

from z3 import *
s = Solver()

modulus = 2**31
sequence = [4096, 618876929, 113892918, 1048278319]

a = Int('a')
c = Int('c')

s.add(0 <= a, a < modulus)
s.add(0 <= c, c < modulus)

for i in range(len(sequence) - 1):
    s.add(sequence[i+1] == c + (a * sequence[i]) % modulus)

if s.check() == sat:
    model = s.model()
    print(f"a = {model[a]}")
    print(f"c = {model[c]}")

これはa = 22695477, c = 1を返します。これは古いBorland C++コンパイラのRNGです。これはおもちゃの例にすぎませんが、同じアプローチは線形帰還シフトレジスタやメルセンヌ・ツイスタでも通用します。

定理を証明する

Z3のリポジトリでは、Z3は定理証明器と呼ばれています。つまり、数学における定理が真であることを証明できるはずです。

これは「論理的双対性」と呼ばれる性質に基づいています。「足し算は可換である」という定理、すなわちall a, b in Real: a + b = b + aを例に取りましょう。これは「!(a + b == b + a)となるa, bは存在しない」と言うことと論理的に同値です。そこでZ3に否定を解かせることができます。反例が見つからなければ、その定理は真ということになります。

from z3 import *

s = Solver()

a, b = Reals('a b')
theorem = a + b == b + a

if s.check(Not(theorem)) == sat:
    print(f"Counterexample: {s.model()}")
else:
    print("Theorem true")

# Prints Theorem true

通常、定理には「a != 0ならば、a * b == 1となるbが存在する」のような条件が付きます。数学者ならこれをa != 0 => some b: a*b == 1と書くでしょう。Z3ではp => qはImplies(p, q)と書き、これを通常どおり否定します。

from z3 import *
s = Solver()

a, b = Reals('a b')
theorem = Implies(a != 0, Exists(b, a*b == 1))
if s.check(Not(theorem)) == sat:
    print(f"Counterexample: {s.model()}")
else:
    print("Theorem true")

これは「Theorem true」を返します。定理を証明できることで、SMTソルバーは形式的検証にとって絶対に欠かせない存在となっています。プログラミング上の関数をZ3の等式の集合に変換できれば、その関数が期待される性質を持つことを証明できるのです。

株を選ぶ

これらのZ3の例をすべて作っていたのと同時期に、私はMiniZincのような汎用制約ソルバー向けの例も書いていました。その際のカスの一部はニュースレターで共有しました。そのうちのいくつかはZ3の練習として定式化し直したのですが、その中でも一つ面白いものがありました。⁵

1日の株価のリストが与えられたとき、1回買ってその後1回売ることで得られる最大の利益を求めよ。

これは十分シンプルに見えます。

arr = [3,1,4,1,5,9,2,6,5,3,5,8]
buy, sell = Ints('i j')
opt.add(buy < sell)
opt.maximize(arr[sell] - arr[buy])

そしてこうなります。

TypeError: list indices must be integers or slices, not ArithRef

問題は、Z3がSMT変数をPython配列のインデックスとして使えないことです。代わりにZ3には「配列の理論」があり、配列をZ3変数として追加できるということです。

from z3 import *
opt = Optimize()

arr = [3,1,4,1,5,9,2,6,5,3,5,8]
arr_z3 = Array('A', IntSort(), IntSort())
for i, v in enumerate(arr):
    opt.add(Select(arr_z3, i) == v)

buy, sell = Ints('i j')
opt.add(buy < sell)

opt.maximize(Select(arr_z3, sell) - Select(arr_z3, buy))
if opt.check() == sat:
    m = opt.model()
    buy_val = m.evaluate(arr_z3[buy])
    sell_val = m.evaluate(arr_z3[sell])
    profit = m.evaluate(sell_val - buy_val)
    print(f"buy at {m[buy]} for {buy_val}")
    print(f"sell at {m[sell]} for {sell_val}")
    print(f"profit: {profit}")

ここまでは順調です。しかし今度は新たな問題が出てきます。

buy at 21237 for -2
sell at 21238 for 0
profit: 2

何が起きているのかを理解するには、SMTの配列が実際には「何」なのかを理解する必要があります。配列は実際にはキーと値のマップに近いものです。キーの「ソート」（要するに型）と値のソートを取ります。つまり私たちの「配列」arr_z3は整数から整数へのマッピングなのです。配列はSelect(A, i)とStore(A, i, val)演算子（新しい配列を返す）も持たなければなりません。⁶ SMTの演算はすべての可能な入力に対して全域でなければならないため、Select(A, i)はiが何であれ値を返さなければなりません。こうしたことから、配列には私たちが意図的に制約しない限り「長さ」や「境界」という概念がないのです。これは有効なZ3プログラムです。

arr = Array('A', IntSort(), IntSort())
s = Solver()
s.check(Select(arr, 3) > Select(arr, -9))
print(s.model())

私の環境では[A = Store(K(Int, -1), 3, 0)]と出力されます。これは「すべての整数を-1にマップするが、3だけは0にマップする配列」という意味です。

これで、なぜZ3が21237で株を買えたのかが説明できます。問題を正しくモデル化するには、buyとsellを、明示的に値を定義したインデックスの範囲に制限しなければなりません。

 opt.add(buy < sell)
+ opt.add(0 <= buy, sell < len(arr))

これで正しく最大利益8が返るようになります。

（無限の配列が何の役に立つのか？文字列から整数へのマップである配列は、String -> Int関数と等価です。これはZ3が制約を満たす関数を見つけられることを意味します！とはいえ、私自身が本気で使ったことはありませんが。）

本に採用したもの

SMTの例を作るにあたって、私には3つの目標がありました。論理が初めての人にも理解できること、一部の読者が仕事で遭遇しそうな実用的な問題に見えること、そしてSMTソルバーがそれを解くのに適したツールであることです。そして上の例のほとんどは、これらのうち少なくとも1つを満たしていません。

• 仕事で数のトリプルを探す必要がある人はいません。
• RNGのリバースをデモするには、PRNGやLCGについて多くの時間を割いて説明しなければなりません。
• 従来の制約ソルバー（同じ章で扱っています）は、数値最適化問題をSMTソルバーよりもはるかに高速に解くことができます。

結局、私は3つの例に落ち着きました。

1. 制約ソルバーではできない最適化問題。ほとんどのソルバーは数値しか扱えないので、「最長共通部分文字列を見つける」は良い選択です。
2. 非常に単純な数学的性質の証明。主に（3）の動機付けのためです。
3. 単純なPython関数の形式的検証。

また、ビットベクターで表現される「マシン整数」に関する制約をZ3が解けることを示す簡単なスクリプトも書きました。

これらが本当に良い選択だったかどうかは、今後のフィードバックでわかるでしょう！

その他の例とZ3のリソース

本では扱わなかった例が他にもいくつかあります。

• テストケースをパスする多項式の導出
• LinkedInのQueensを解く

他の人の例：

• Andrew Helwerのファイアウォール等価性
• Nelson Elhageのクロスワードソルバー
• Hakan Kjellerstrandのパズルとトイモデル

その他のリソース：

• 開発者によるz3pyチュートリアル
• Microsoft ResearchのオンラインZ3ガイド。SMT-LIBチュートリアルでは、Python SDKではサポートされていない最新のZ3機能も紹介されています。
• Z3が準拠しているSMT-LIB標準。

Nelson Elhageにフィードバックをいただきました。この投稿が気に入ったら、ぜひニュースレターにご登録ください！毎週新しいエッセイを書いています。

私の著書Logic for Programmersはついに内容が完成しました！技術レビュアーからのフィードバックを待つ間、現在のベータ版と今後のアップデートをこちらから20%オフで入手できます。

追記 2026-02-26

Jeremy Salwenが、定理の例では結果がsatでなければunsatに違いないと仮定しているが、SMTソルバーはどちらも返さないことがあると指摘してくれました。私のミスです！代わりにチェックは次のように書く必要があります。

result = s.check(Not(theorem))
if result == sat:
    print(f"Counterexample: {s.model()}")
elif result == unknown:
    print("Could not prove or disprove theorem")
else:
    print("Theorem true")

これはz3.proveユーティリティ関数がおおよそどのように定義されているかを示しています。

1. Python APIはSMT-LIBにコンパイルされるゆるいレイヤーです。実際にソルバーに渡されるものを見たい場合は、スクリプトの末尾にprint(s.sexpr())を追加してください。 [return]
2. これらはPython APIが提供する高水準なユーティリティ関数であることに注意してください。実際に生成されるZ3コードではProd(lhs)は単に(* (lhs__0 lhs__1 lhs__2))にインライン展開されます。 [return]
3. 厳密に言えば、これは代数的数です。Realには2の平方根は入れられますが、例えば円周率πは入れられません。 [return]
4. Z3のコアエンジンはC++で書かれているのに、手書きのPythonによる二分探索の方が最適なcを約1000倍も速く見つけられます！Z3での最適化は本当に遅いのです。 [return]
5. あのニュースレターとこの投稿の間に、Abdul Rahman SibahiがA Dumb Introduction to z3を書いてくれました。そこではニュースレターのお釣りカウンター問題がZ3に移植されています。なので私はそれを書く必要がなくなりました！ [return]
6. Python APIはA[i]をselect(A, i)に糖衣構文を剥がします。つまり最適化の目標をarr_z3[sell] - arr_z3[buy]、制約のループを[arr_z3[i] == arr[i] for i in range(len(arr))])と書くこともできたということです。ここでは透明性のためにあえてselectを使いました。 [return]