在撰写 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 最常见的方式：实例化一个求解器，向其中添加约束，然后检查。¹ Ints('x y') 会创建两个“常量”。当我们调用 s.check() 时，求解器会尝试为这些常量找到满足所有约束的值（即模型）。在这里，它会打印出“sat”，后面跟着 [x = 2, y = 3]。如果有多个解，它会返回找到的第一个；如果无解，则会打印“unsat”。

不管怎么说，这就是“可满足性”部分的含义。而“模理论”部分则源于 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”，意味着不存在这样的一对数对。回想起来我本该料到这个结果；证明请看下方的折叠内容。

如果我们用两个不同的三元组来尝试呢，也就是六个互不相同的数？我可不想写十五条互不相等的语句，所以来用点语法糖：

• 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。

最小化年度存款

相比 MiniZinc 这类专用约束求解工具，Z3 的优化器要慢得多，MiniZinc，但我们仍然可以用它来解决一些简单问题。

一个银行账户提供 1% 的年化收益率。要在 20 年后拥有 10000，需要每年最少存入多少？假设存款发生在利息结算之后。

那么第一年我们有 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 有点像无限精度的浮点数。³ r 必须是 RealVal，因为它是一个固定值，而不是需要 Z3 去求解的东西。这段代码会计算 20 年后 balance 的最终值。

话虽如此，这种做法意味着我们无法知道第 14 年时 balance 的值是多少。如果想要中间结果，我可以把 balance 做成一个包含 20 个实数的数组，其中 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() 时传入额外的约束。直到最近我才知道还可以这么做！如果想求解同一个问题的多个实例，这似乎很有用，不过就我所见，人们更倾向于每次都实例化新的求解器对象，而不是用新约束去“参数化”同一个求解器。

逆向破解随机数生成器

写这本书时，我特别想确保引入的每个主题都有实际的应用。它不必让每个程序员都感兴趣，只要足够有用，能让人觉得“我能想象学这个会对某些人有帮助”就好。这促使我写了一个关于逆向推导随机数生成器取值的例子。

软件中的大多数随机数生成器实际上是伪随机的：它们使用确定性的数学算法来生成一串在大多数使用场景下“足够随机”的数字。我在这里更详细地讨论过这一点。其中一种算法是 线性同余生成器（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++ 编译器的随机数生成器。这只是一个玩具例子，但同样的方法也适用于线性反馈移位寄存器和梅森旋转算法。

证明定理

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 这类通用约束求解器编写示例。我在 newsletter 上分享了其中的一些边角料。我还把其中几个用 Z3 重新形式化了一下以作练习，其中有一个显得特别有意思：⁵

给定一天中一系列股票价格，找出通过买入一次并在之后卖出一次所能获得的最大利润。

这看起来足够简单：

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（基本就是类型）和一个值的 sort。因此我们的“数组”arr_z3 是从整数到整数的映射。数组还必须有 Select(A, i) 和 Store(A, i, val) 操作符（后者会返回一个新数组）。⁶ 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 求解器应该是解决它们的合适工具。而上面的大多数例子至少有一条不满足：

• 没有人会在工作中需要去找数字三元组。
• 要演示逆向随机数生成器，我得花大量时间去解释伪随机数生成器和 LCG。
• 传统约束求解器（在同一章中也有介绍）求解数值优化问题的速度要比 SMT 求解器快得多。

最后我选定了三个例子：

1. 一个约束求解器做不到的优化问题。大多数求解器只能处理数字，所以“寻找最长公共子串”是个不错的选择。
2. 证明一个非常简单的数学性质，主要是为了引出第（3）个例子
3. 对一个简单的 Python 函数进行形式化验证。

我还写了一个小脚本来展示 Z3 可以求解关于“机器整数”的约束，这类整数是用位向量来表示的。

这些选择到底好不好，就看读者的反馈了！

其他示例与 Z3 资源

还有几个我没放进书里的例子：

• 推导出能通过测试用例的多项式
• 求解 LinkedIn 上的 Queens 谜题

其他人的示例：

• Andrew Helwer 的 Firewall Equivalence
• Nelson Elhage 的 Crossword Solver
• Hakan Kjellerstrand 的 谜题与玩具模型

更多资源：

• 作者本人的 z3py 教程
• Microsoft Research 的 在线 Z3 指南。其中的 SMT-LIB 教程还展示了 Python SDK 尚未支持的现代 Z3 特性。
• Z3 所遵循的 SMT-Lib 标准。

感谢 Nelson Elhage 提供的反馈。如果你喜欢这篇文章，欢迎订阅我的 newsletter！我每周都会在上面发布新文章。

我的书 Logic for Programmers 现已内容完结！在等待技术审校反馈期间，你可以在此以八折优惠获取当前的 Beta 版以及未来的更新。

更新 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 只是一个编译到 smtlib 的松散封装层。如果你想看看实际喂给求解器的内容，只需在脚本末尾加上 print(s.sexpr()) 即可。 [返回]
2. 注意这些是 Python API 提供的高层便捷函数。实际生成的 Z3 只是把 Prod(lhs) 内联为 (* (lhs__0 lhs__1 lhs__2))。 [返回]
3. 严格来说，它实际上是一个代数数。你可以把 2 的平方根塞进 Real 里，但比如 Pi 就不行。 [返回]
4. Z3 的核心引擎是用 C++ 写的，然而一个手写的 Python 二分查找寻找最优 c 的速度却要快大约 1000 倍！Z3 的优化真的很慢。 [返回]
5. 在那篇 newsletter 和本文之间，Abdul Rahman Sibahi 写了 A Dumb Introduction to z3，其中包含了 newsletter 里找零计数问题的 Z3 版本。所以我就不用再写那个了！ [返回]
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。 [返回]