Z3求解器实战教程：从安装到约束求解与避坑指南

简介：Z3是微软开发的SMT（可满足性模理论）求解器，广泛应用于软件/硬件验证、程序分析与形式化推理。这份PDF教程从理论基础讲起，清晰解释数组理论、算术理论等背景理论，并结合升降序数组、加法交换律等示例说明可满足性与解的含义。教程重点介绍Z3的Python API用法，给出完整的Solver定义、约束添加与模型求解代码示例，并覆盖Linux、Windows、macOS下从源码编译与二进制安装两种方式，附GitHub仓库、官方编程指南及Stanford课程等延伸学习资源。资源共1个PDF文件，压缩包大小518KB，内容精炼，适合刚接触SMT求解或希望在Python中集成Z3的开发者快速入门。已有86人学习下载，适合作为自动化推理、程序验证等方向的便携速查手册。

1. Z3 不是解压软件：这份 PDF 背后是一套能证明逻辑问题的求解器

第一次看到“Z3使用教程.pdf”这个文件名，老读者可能会愣一下：Z3 不是微软研究院那个自动定理证明工具吗？怎么还出 PDF 了。没错，你搜到的这份教程，核心对象就是 Z3 求解器——一个用于可满足性模理论（SMT）的高性能引擎。它的典型用途包括：验证程序断言、破解加密算法、调度排课、求解数独、分析符号执行路径，甚至给优化问题找可行解。适合的人群很明确：写编译器、做安全分析、搞算法竞赛、以及所有被“组合爆炸”逼到墙角，想用一个黑盒把约束求解掉的工程师。我这篇文章不念 PDF，只把它背后真正能落地的使用链路讲透：装好、跑通、会调参、知道坑在哪。

2. 安装与环境准备：用 pip 还是源码，别在这些地方白费半小时

2.1 最快路径：pip 安装 z3-solver

Z3 官方提供 Python 绑定，PyPI 包名是z3-solver，不是z3。这一步很多人栽了跟头——pip install z3会装到一个无关的库，导致from z3 import *直接报ModuleNotFoundError。正确的是：

pip install z3-solver python -c "from z3 import *; print(get_version_string())"

命令逻辑：第一行安装绑定库，第二行验证版本。get_version_string()是 Z3 提供的全局函数，返回如4.13.0这样的版本号。如果你在公司内网用镜像源，记得加-i https://pypi.tuna.tsinghua.edu.cn/simple这类参数。注意：z3-solver自带 C++ 动态库，不需要单独装 VSCode 或 visual studio 运行库，Linux 和 Windows 都能开箱即用。

2.2 为什么不建议源码编译

很多人迷信git clone https://github.com/Z3Prover/z3然后python scripts/mk_make.py编译。其实日常用 Python 做约束求解，完全没必要。源码编译的时间足够你跑通五个验证样例了，而且还会踩到 CMake 版本、C++ 编译器 ABI 不匹配之类莫名其妙的坑。我一般只会在需要定制求解策略、修改 Z3 内部算法、或者给 Java/Go 这种非 Python 语言写绑定时才碰源码。Linux 用户如果是系统级安装，还要注意pip install --user和sudo pip install的权限之争，建议用虚拟环境：

python -m venv z3env source z3env/bin/activate # Windows 下用 z3env\Scripts\activate pip install z3-solver

venv的参数按需加，隔离是重点。装到虚拟环境里，以后升级、卸载、换版本都不会污染系统 Python。如果你用的是 Anaconda，也可以conda create -n z3 python=3.10再pip install，但 conda 默认频道里的z3老版本可能不兼容 Python 3.11，少给 pip 找麻烦。

2.3 版本差异：API 别混用，优先 4.x 稳定分支

Z3 的 Python API 在稳定分支上保持兼容，但也有微调。例如Solver().set()在旧版参数叫params，新版叫**params。最稳的做法是锁住你安装时的版本，在requirements.txt里写死：

z3-solver==4.13.0

升级前看看CHANGES.md。还有一点常踩坑：z3.z3const模块里边很多下划线开头函数是私有 API，不要依赖。如果网上教程用的是Tactic、Goal这些高层接口，4.x 都能用；但如果看到Solver.solve()或Solver.model()这种返回值直接当字典用的写法，多半是老版本教程——现在model()返回的是ModelRef，需要用s.model().eval(expr)来取值。后面第三、四章我用到的方法，都基于 4.x。

2.4 验证安装是否正常的三个基准测试

装完最怕的是“能 import 但算不对”。我习惯跑三个最小用例：一个sat、一个unsat、一个BitVec算术。下面这段脚本可以一次验证：

from z3 import * # 用例1：基础整数约束 x = Int('x') s = Solver() s.add(x > 3, x < 10) assert s.check() == sat print("用例1 ok:", s.model()[x].as_long()) # 用例2：矛盾约束 s2 = Solver() s2.add(x > 5, x < 2) assert s2.check() == unsat print("用例2 ok") # 用例3：位向量加法溢出 b = BitVec('b', 4) s3 = Solver() s3.add(b + 1 == 0) # 4位无符号，b应为15 assert s3.check() == sat assert s3.model()[b].as_long() == 15 print("用例3 ok:", s3.model()[b].as_long())

三个用例分别覆盖了基本算术、逻辑判定和位向量语义。assert是为了让错误暴露得更早——如果你某个环境里 Z3 的 BitVec 溢出语义不对，会立刻抛异常。这里还有一个隐藏细节：BitVec('b', 4)的取值范围是 0 到 15，b + 1 == 0在模 16 下成立，所以b能取 15。如果你预期它应该无解，那是你把位向量和数学整数搞混了。

3. 核心概念与第一个最小可行程序：从表达式到 SAT/SMT 模型

3.1 理解 Z3 的“排序”而不是“类型”

Z3 的世界观里，每个表达式都有排序，相当于类型系统的泛化。IntSort是整数，RealSort是实数，BoolSort是布尔，BitVecSort(n)是 n 位位向量。你写x = Int('x')时，x是一个声明符，它还不是值；当你把它加进Solver，Z3 会去寻找一个能让所有约束同时成立的值指派。如果找到了，状态是sat，并且model()给出一组指派；如果找不到，状态就是unsat。最容易被忽略的是：Int和Real混用会导致算术运算隐式转换，某些情况下能解，某些情况下会把问题变成非线性实数算术，直接进入unknown。

来看第一个最小例子：

from z3 import * x = Int('x') y = Int('y') s = Solver() s.add(x + y == 10) # 约束1 s.add(x > 3) # 约束2 s.add(y < 8) # 约束3 if s.check() == sat: m = s.model() print("x =", m[x].as_long()) # 注意 as_long() print("y =", m[y].as_long()) else: print("无解:", s.unsat_core())

这段代码的逻辑：声明两个整数变量，创建一个默认求解器，使用add()依次追加约束。check()返回sat后，model()中的m[x]是一个IntNumRef对象，必须调用.as_long()转成 Pythonint才能用于打印或后续计算，直接拿去加减会报类型错误。unsat_core()只在设置unsat_core_proof=true时可用，否则返回空列表。这里我们能看到 Z3 的核心工作流程：声明→断言→检查→取模型。

3.2 约束不满足时怎么取证：unsat 与模型不存在的区别

如果s.check()返回unsat，意味着约束集合互相矛盾。这时s.model()会抛异常，很多人这里翻车。正确姿势是先保存 check 返回值再决定是否取模型。还有种情况是check()直接返回unknown，说明求解器在给定时间内没能力判断，这不代表无解，只是被理论复杂度卡住了。常见做法是设置超时或更换理论。比如要求用“整数线性算术”求解，可以显式指定逻辑标签：

set_option('smt.arith.solver', 2) # 使用新的算术求解器

set_option是全局选项，等价于命令行-smt.arith.solver:2。第 2 个参数控制算法内部选择，改这个能影响非线性整数算术的启发式。但如果问题本身是纯线性，默认配置就够了。遇到unknown时，第一反应应该是看s.reason_unknown()，返回值如"smt tactic failed to show goal to be sat/unsat"或"timeout"，这是排查问题的钥匙。

3.3 如何快速验证一个模型是否正确

拿到m之后别急着相信，手动代入原约束做一次检查是血泪教训。我自己的习惯是写一个断言函数：

m = s.model() assert m[x].as_long() + m[y].as_long() == 10 assert m[x].as_long() > 3 assert m[y].as_long() < 8 print("模型验证通过")

这三个断言就是你把求解结果回带到原始约束里做确认。虽然 Z3 理论上不会给错模型，但当你使用Optimize、PartialModel或者自定义model_completion时，完全可能拿到缺失项。而且一旦后续你替换了add()的顺序或者修改了约束，这个断言能立刻拦住低级错误。还有一点，很多人喜欢把m[x].as_long()存到变量里，我建议每次都显式调用，因为如果变量是Real，as_long()会抛异常，改成approx()或as_fraction()才能正确处理。

3.4 常用表达式构造器和它们的真实身份

Z3 里的逻辑连接词不是 Python 的and/or/not，而是And/Or/Not。为什么？因为 Python 的布尔运算会强制把左侧值转换成bool，而 Z3 的表达式是BoolRef，并没有实现__bool__，所以s.add(x > 0 and x < 10)这种写法会直接报错：“ArithRef不能转换”。正确写法是s.add(And(x > 0, x < 10))。类似的还有Implies(a, b)表示蕴含，If(cond, a, b)表示条件表达式，以及Distinct表示一组值互不相同。在写约束时，我建议把“逻辑连接词”和“业务约束”分开想：业务约束是数学关系，连接词是它们之间的组合方式。如果遇到Tactic控制求解过程，还可以用Then、Repeat这些组合器，但日常用Solver就够了。

4. 三个能直接抄作业的实际场景：数独、符号执行和整数优化

4.1 数独求解：用 81 个约束等价于一条逻辑

数独是 Z3 教程里最经典的入门案例，原因是它把“声明变量+约束”的思路表达得很干净。我们用Int('cell_{r}_{c}')声明 81 个整数变量，每个变量范围 1-9，再按行、列、宫加约束。下面这个实现可以直接跑：

from z3 import * # 空白格用 0 表示，提前给一个 9x9 的待求盘面 board = [ [5, 3, 0, 0, 7, 0, 0, 0, 0], [6, 0, 0, 1, 9, 5, 0, 0, 0], [0, 9, 8, 0, 0, 0, 0, 6, 0], [8, 0, 0, 0, 6, 0, 0, 0, 3], [4, 0, 0, 8, 0, 3, 0, 0, 1], [7, 0, 0, 0, 2, 0, 0, 0, 6], [0, 6, 0, 0, 0, 0, 2, 8, 0], [0, 0, 0, 4, 1, 9, 0, 0, 5], [0, 0, 0, 0, 8, 0, 0, 7, 9], ] X = [[Int(f"cell_{r}_{c}") for c in range(9)] for r in range(9)] s = Solver() # 取值范围 for r in range(9): for c in range(9): s.add(And(X[r][c] >= 1, X[r][c] <= 9)) # 给定数字 for r in range(9): for c in range(9): if board[r][c] != 0: s.add(X[r][c] == board[r][c]) # 行、列、宫不重复 for i in range(9): s.add(Distinct(X[i])) # 第 i 行 s.add(Distinct([X[r][i] for r in range(9)])) # 第 i 列 for br in range(0, 9, 3): for bc in range(0, 9, 3): cells = [X[r][c] for r in range(br, br+3) for c in range(bc, bc+3)] s.add(Distinct(cells)) if s.check() == sat: m = s.model() for r in range(9): row = [str(m[X[r][c]]) for c in range(9)] # 这里不是 as_long()，会得到字符串 print(" ".join(row)) else: print("无解")

这套代码里的关键函数是Distinct，它保证一组值两两不同。注意取模型时我用了str(m[X[r][c]])，因为Int的模型项本身可以被str()转成可读形式。但如果你想做算术运算，就必须as_long()。这段逻辑说明：数独问题是把每个格子的候选值当成整数约束，And连接范围，Distinct处理排他性。实际跑出来大约几十毫秒到几百毫秒，如果加了宫约束都还没解，多半是前面对board的索引写错了——比如第 8 行第 9 列是X[7][8]，别把行列反过来。另外，如果你想求所有解，可以用while s.check() == sat循环，每次输出解后追加一个Or(...)排除当前解，但那样会很快爆炸，不建议。

4.2 符号执行：不是猜输入，是找到一条到达崩溃的路径

做安全分析或逆向工程时，常需要回答“给定某个分支条件，能否找到使程序走到目标分支的输入”。Z3 擅长这种约束生成。假设有一个简单的整数校验函数：如果输入x满足x*x < 10且x > 2，程序会进入危险分支。我们想知道是否存在这样一个x：

from z3 import * x = Int('x') s = Solver() s.add(x > 2) # 前置条件 s.add(x * x < 10) # 危险分支条件 if s.check() == sat: m = s.model() print("可以到达危险分支，x =", m[x].as_long()) else: print("无法到达")

这个例子很简单，但注意x * x < 10是乘法表达式，属于非线性整数算术。对某些非线性约束，Z3 可能返回unknown。遇到这种情况，常见做法是限定求解逻辑：

set_option('smt.arith.solver', 6) # 强力非线性策略

实际上，Z3 处理非线性整数是将其转化为有限域上的搜索，能力有限。真正靠谱的做法是把x声明成实数Real('x')再求解，实数上的非线性算术能力要强很多，但带来的模型就可能是小数，不一定符合程序输入类型。工程上常用技巧是：先用Real求解得到可行区间，再在区间内枚举整数。这是符号执行工具中常见的“整数解回退”策略。

4.3 优化问题：用 Optimize 找最大值，不只是可行解

默认的Solver只回答“能不能满足”，不回答“哪个解最优”。如果你要找x + y的最大值，就得用z3.Optimize。经典示例是：

from z3 import * x = Int('x') y = Int('y') opt = Optimize() opt.add(x >= 1, x <= 5) opt.add(y >= 2, y <= 8) opt.maximize(x + y) if opt.check() == sat: print("目标值 =", opt.model().eval(x + y).as_long()) else: print("无解")

maximize会隐式创建一个目标函数，check()内部可能多次调用底层求解器寻找边界。注意opt.model().eval(x + y)返回的是目标值，但要拿到具体x、y，还是得opt.model()[x].as_long()。这个例子中最大值是 13（x=5,y=8）。Optimize是Solver的增强版，它支持minimize、maximize，以及多个目标的优先级设定（软硬约束）。商业调度、资源分配这类问题，用它能省不少手写搜索的功夫。不过要注意，Optimize底层跑的是多个Solver实例，如果约束很多，会比普通Solver慢一个数量级。如果只是要一个可行解中的最优边界，建议先Solver找到可行解，再手动加目标等式迭代收紧。

5. 避坑指南：五个最容易让新手放弃 Z3 的坑

5.1 现象：int与z3.Ref直接加减，抛TypeError或返回奇怪的表达式

原因：Z3 重载了__add__，你写m[x] + 1，这里m[x]是IntNumRef，它返回的是一个新的ArithRef表达式，而不是 Python 整数，直接拿去print或和整数比较会不对。解决：先用.as_long()转成 Python 原生类型。只有当x是 Z3 声明的变量时，x + 1才是一个合法的 Z3 表达式；当x是从模型里取出来的值时，它已经绑定到具体常量，此时再和运算需要转换。

举例：

m = s.model() x_val = m[x].as_long() if x_val + 1 > 3: # 这里 x_val 是 int print("OK")

5.2 现象：Solver()求解大规模问题变得极慢，甚至check()卡住不动

原因：没有限制求解时间，或用错理论。比如把Int变量当索引去访问数组，Z3 内部会尝试展开很多分支。解决：设置超时是一个很暴力的手段：

s.set(timeout=10000) # 毫秒 if s.check() == sat: ... else: reason = s.reason_unknown() if reason == "timeout": print("超时，换个策略")

在s.check()前调用s.set(timeout=...)，底层会启动超时机制。对于长时间无解的问题，先让程序不彻底卡死，再考虑放松约束或者换理论。另外，尽量避免在约束里使用除法IntVal(1)/x这种会产生 Real 转轮的表达式，直接变成乘法约束，求解速度天壤之别。

5.3 现象：bool和BoolRef混用，条件分支老是出问题

原因：Z3 的And、Or、Not需要BoolRef，而 Python 的and、or会把表达式当作真值判断，直接告诉你“表达式是 arith ref 不能转 bool”。解决：永远在约束外面用 Z3 函数。如果已经写了s.add(x > 0 and x < 10)，这里x > 0 and x < 10会被 Python 先求值成(x > 0) < 10再抛异常。正确写法是s.add(And(x > 0, x < 10))。

5.4 现象：获取模型后，所有值都变成None

原因：当一个变量没有被任何约束限制时，Z3 可能不为它生成模型指派。默认Solver.model()可以返回部分模型，缺失的项就是None。解决：在check()后使用s.model().eval(var, model_completion=True)，第二个参数会要求求解器补齐剩余的变量。注意model_completion并不总是有效，但对变量未约束的简单情形够用。另一种办法是加上s.add(Or(x == 0, x == 1))之类的策略性约束，让每个变量都有显式范围。

5.5 现象：非线性整数算术问题一直unknown

原因：Z3 对非线性整数算术用的是不完全算法，很多问题的判定本质上是不可判定的，或者计算复杂度极高。解决：明确判断问题类型。如果变量必须为整数，尽量把非线性项化简成线性：比如把x*y当做一个新变量z，然后加约束z == x*y，但这不能从根本上降低难度。常见做法是先用Real求解得到可行域，再用区间枚举整数候选值。我在实际项目中，遇到商品价格、库存数量这类整数模型，都倾向于把非线性约束展开成有限候选集，然后用BitVec做位运算表示，出奇地快。

6. 进阶技巧：用 Z3 验证自己的手写逻辑，以及处理混合理论

6.1 一个技巧：用Prove简化表达式，验证方程组等价性

Z3 不仅能求模型，还能做表达式级别的化简。比如你写了两个表达式，想知道它们在所有给定条件下是否等价，可以用Prove：

from z3 import * x = Int('x') y = Int('y') f1 = (x + y) * (x - y) f2 = x * x - y * y Prove(f1 == f2)

Prove实际上是判断f1 != f2是否unsat。如果打印proved，表示等价成立。这个技巧在做代数恒等式验证、简化编译器优化时特别有用。我自己碰到的例子：手写了一个整数溢出检测函数，把它和位向量语义下的标准表达式做Prove，立刻发现了一个符号位判断错误。这种验证不需要构造输入，完全形式化。

6.2 混合理论：BitVec 和 Int 的边界，别用错了排序

很多业务场景里，变量既涉及整数算术，又涉及位操作。比如分析一个计数器溢出逻辑：

from z3 import * b = BitVec('b', 8) # 8 位无符号符号位向量 s = Solver() s.add(b + 1 == 255) # 无符号字节加法 if s.check() == sat: print(s.model()[b].as_long()) # 输出 254

这里如果用Int描述b+1==255，会得到b==254，但如果是 8 位溢出语义，b==255时b+1==0，约束就无解。Z3 对BitVec的加法默认是模2^n的。选择排序取决于你的真实语义：网络协议解析、密码学、底层二进制分析必须用BitVec；离散数学、规划排程用Int。混用会触发隐式转换，产生不可预期的结果。我在做二进制漏洞分析时，经常在一份约束里同时用BitVec表示寄存器，用Int表示循环次数，然后通过zero_ext、sign_ext或Extract搭桥。

6.3 学会给模型做回归校验，是“不翻车”的最后一道防线

前面已经提到过手动验证模型，这里补充一个通用做法：把求解结果导出成 JSON，再用原始约束脚本独立重读一遍。这样即使 Z3 内部有 bug 或配置异常，你也能在集成测试里发现。我的习惯是在生产环境的求解封装函数里加一个verify参数：

def solve_with_verify(constraints, vars, timeout=5000): s = Solver() s.add(constraints) s.set(timeout=timeout) r = s.check() if r == sat: m = s.model() for c in constraints: if not is_true(m.eval(c, model_completion=True)): raise ValueError("模型验证失败，约束未被满足: {}".format(c)) return m return None

m.eval(c, model_completion=True)会把每个约束表达式放到模型下求值，返回BoolRef；如果结果是False，说明模型不满足该约束。这段代码相当于给你的上层算法加了双保险。

说实话，我最初用 Z3 时吃过大亏：在解一个整数规划问题时，没做回归校验，直接信了模型，结果上线后数据对不上，排查了半天才发现是我把一个Real变量误当成Int，模型给出的值带小数，导致业务判断全错。后来我所有求解代码都强制加校验，宁可慢几十毫秒，也要把“模型自洽”这件事锁死。这才是我最想分享的心得：Z3 很强，但它只是一个推理引擎，业务逻辑的正确性还是要靠你自己去验证。希望这篇教程能帮你少走弯路，把时间留给真正的问题，而不是和求解器本身搏斗。希望帮到你。

本文还有配套的精品资源，点击获取