我寫的幾個有點無聊的 Z3 腳本
原文由 Hillel Wayne 于 發布，訂閱此部落格
在撰寫 Logic for Programmers 的過程中，我產生了大量的「邊角料」——寫好又丟掉的程式碼範例和章節。有時候是為同一個主題找到了更好的例子，有時候則是整個主題都不要了。讓這些東西全爛在硬碟裡感覺有點可惜，所以我決定把其中一批跟一個叫做「Z3」的工具有關的邊角料分享出來，它在軟體研究中有各式各樣的用途。
首先會說明這個工具到底是什麼，接著再依照有趣程度遞增的順序分享一些腳本。所有範例都會使用 Python 綁定（pip install z3-solver）。
什麼是 Z3？
Z3 是一個 SMT 求解器。
好，那什麼是 SMT？
SMT（「Satisfiability Modulo Theories」，可滿足性模理論）求解器是一種懂數學和基本程式概念的約束求解器。你給它一些變數、一些包含這些變數的方程式，它會試著幫你找出一個模型，也就是一組能同時滿足所有方程式的賦值。
想像你 12 歲，第一次上代數課，看到這樣一題：
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 用法：建立一個求解器、加入約束，然後檢查它。1 Ints('x y') 會建立兩個「常數」。當我們呼叫 s.check() 時，求解器會試著為這些常數找出能滿足所有約束的值（也就是模型）。在這裡它會印出「sat」，接著是 [x = 2, y = 3]。如果有多組解，它會回傳第一個找到的；如果無解，就會印出「unsat」。
以上就是「可滿足性」的部分。至於「模理論（Modulo Theories）」的部分，則是指 Z3 內建了一堆針對不同領域、也就是不同「理論」的專門求解器。這讓它能處理涉及陣列、正則表達式、量化表達式等各種約束。
接下來我們就跟潮人一樣，把整個 Z3 API 直接匯入命名空間。
腳本集
我曾想過的一個無聊數學問題
是否存在四個相異的正整數
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」，表示不存在這樣的數對組合。回頭想想我早該料到這個結果；證明請見下方的下拉選單。
顯示證明
要讓 (a, b) 和 (c, d) 的和相同，必定存在某個 e 使得 (c, d) = (a + e, b - e)。那麼 cd = (a+e)(b-e) = ab + be - ae - ee，只有當 ee = e(b-a)，也就是 e = b - a 時，才會等於 ab。再把這個代回去，就得到 (c, d) = (a + b - a, b - b + a) = (b, a)。
Nelson Elhage 也指出，這個問題有個幾何詮釋：「是否存在兩個不全等、但周長與面積都相同的長方形？」
那如果我們試試兩組相異的三元組，也就是六個相異的數字呢？我可不想寫十五個不相等判斷，所以來用點語法糖：
IntVector('lhs', 3)會回傳變數列表[lhs__0, lhs__1, lhs__2]。Sum和Product的作用就跟你想的一樣。2Distinct(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。
最小化每年投入金額
跟 MiniZinc 這種專門的約束求解工具相比，Z3 的最佳化器要花很久的時間，但我們還是可以用它來解一些簡單的問題。
一個銀行帳戶提供 1% 的年收益率。要在 20 年後擁有 10,000 元，每年最少要存入多少？假設存款是在利息入帳後才存入。
所以第一年我們有 C 元，第二年有 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這次我們用的是 Real 而不是 Int。Real 有點像是無限精度的浮點數。3 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 常用的用途，因為它真的很慢，但仍然是個相當酷的功能。4
這也展示了一個有用的技巧：我們可以在呼叫 check() 時傳入額外的約束。我也是最近才知道可以這樣做！這在需要求解同一個問題的多個實例時似乎很有用，不過就我觀察，大家還是比較偏好每次都建立新的求解器物件，而不是用新的約束去「參數化」同一個求解器。
逆向工程隨機數產生器
我在寫這本書時，有一件事特別想做到：確保每個介紹的主題都有實際的應用。不一定要讓每個程式設計師都覺得有吸引力，只要實用到讓人覺得「我看得出來學這個對某些人會有幫助」就好。這讓我寫了一個關於逆向工程 RNG 數值的範例。
軟體中大多數的隨機數產生器其實是虛擬亂數：它們用確定性的數學演算法來產生一串對多數使用情境來說「夠亂」的數字。我在這裡有更詳細的討論。其中一種演算法是 線性同餘產生器（Linear Congruential Generator，LCG）。LCG 有固定的常數（a、c、m）、一個起始種子 X，並用這樣的方式計算下一個值：
X = (a * X + c) % m舉例來說，如果 a = 6, m = 59, c = 0，從 1 開始的序列會是 1, 6, 36, 39, 57 等等。不過大多數實際的序列會使用大得多的數值。我們來寫一個 SMT 問題，給定一個序列和 m，反推出 (a, c)。
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 使得 !(a + b == b + a)」。所以我們可以要求 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，那麼就存在某個 b 使得 a * b == 1」。數學家會寫成 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 的練習，其中有一個特別有趣：5
給定一天中一系列的股價，找出透過買入一次、再於之後賣出來能獲得的最大利潤。
這看起來相當簡單：
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 陣列實際上「是什麼」。陣列其實更接近鍵值對映射：它接受一個鍵的「排序（sort）」（基本上就是型別）和一個值的排序。所以我們的「陣列」arr_z3 是把整數映射到整數。陣列還必須有 Select(A, i) 和 Store(A, i, val) 運算子（會回傳一個新陣列）。6 SMT 的運算必須對所有可能的輸入都是全函數的，也就是說不管 i 是什麼，Select(A, 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 範例有三個目標：對剛接觸邏輯的人來說要好懂、看起來要像是某些讀者在工作中可能會遇到的實際問題，而且 SMT 求解器要是解決它們的合適工具。而上面大多數範例至少不符合其中一點：
- 沒有人需要在工作中尋找數字三元組。
- 要展示逆向工程 RNG，我得花一大堆時間解釋虛擬亂數和 LCG。
- 傳統的約束求解器（在同一章節中也有介紹）最佳化數值問題的速度比 SMT 求解器快得多。
最後我選定了三個範例：
- 一個約束求解器做不到的最佳化問題。大多數求解器只能處理數字，所以「找出最長共同子字串」是個不錯的選擇。
- 證明一個非常簡單的數學性質，主要是為了引出第 3 點
- 形式化驗證一個簡單的 Python 函式。
我還寫了一個小腳本，展示 Z3 可以處理「機器整數」上的約束，這些整數是用位元向量來表示的。
這些到底是不是好選擇，就看讀者的回饋了！
其他範例與 Z3 資源
我還有幾個沒放進書裡的範例：
其他人的範例：
更多資源：
- 原作者的 z3py 教學
- Microsoft Research 的 線上 Z3 指南。SMT-LIB 教學也展示了 Python SDK 尚未支援的現代 Z3 功能。
- Z3 所遵循的 SMT-Lib 標準。
感謝 Nelson Elhage 提供的回饋。如果你喜歡這篇文章，歡迎加入我的電子報！我每週都會在那裡發表新的文章。
我的書 Logic for Programmers 內容已經全部完成了！在等待技術審稿人回饋的同時，你可以在這裡以八折優惠取得目前的測試版以及未來的更新。
更新 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 便利函式的定義方式。
- Python API 是一個編譯成 smtlib 的鬆散層。如果你想看實際餵進求解器的內容，只要在腳本最後加上
print(s.sexpr())就好。 [返回] - 請注意，這些是 Python API 提供的高階便利函式。實際產生的 Z3 只是把
Prod(lhs)內聯為(* (lhs__0 lhs__1 lhs__2))。 [返回] - 嚴格來說，它其實是一個代數數。你可以把根號 2 放進 Real 裡，但不能放像 Pi 這種數。 [返回]
- Z3 的核心引擎是用 C++ 寫的，但一個手寫的 Python 二分搜尋找到最佳
c的速度還要快上大約 1000 倍！Z3 的最佳化真的很慢。 [返回] - 在那封電子報和這篇文章之間，Abdul Rahman Sibahi 寫了 A Dumb Introduction to z3，其中包含了電子報中找零問題的 Z3 轉換版本。所以那題我就不用寫了！ [返回]
- 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。 [返回]
留言
登入後參與討論