Z3 2008 — 把 SMT 工程化到工业默认

是什么

Z3 是 2008 年微软研究院发布的 SMT 求解器——给一堆”逻辑式 + 数学约束”，它判定能不能同时成立、给出例子或证明无解。

日常类比：你跟租房中介说”月租 < 5000、地铁 10 分钟内、面积 ≥ 30 平、押一付一”。中介脑子里跑的就是 SMT——每条都不是单纯真假，而是带”数值/集合/函数”的混合约束。Z3 是这种活儿的工业级引擎。

这篇 TACAS 2008 论文不是发明新算法，而是把过去十几年 SMT 理论一次工程化：nieuwenhuis-dpll-t-2006 的 DPLL(T) 抽象、nelson-oppen-1979 的多 theory 协作、minisat-2003 的 SAT 引擎、e-graph 的 congruence closure、量词 E-matching——全部塞进同一个 C++ 内核，加上 Microsoft 大量经验调出的启发式。

结果：2008 SMT-COMP 横扫多个 division，从此成为工业默认 SMT 引擎。

为什么重要

不理解 Z3 的工程定位，下面这些事都说不清：

为什么 Dafny / F* / Boogie / Lean 4 后端默认是 Z3——不是它最聪明，是它最稳、API 最适合反复 push/pop
为什么 LLM 形式化助手（Lean Copilot / ProofNet 评测 / Aesop）几乎都调 Z3——它有官方 Python 绑定、模型/证明/unsat core 三件套齐全
为什么 符号执行工具（KLEE / SymCC / angr）一边跑路径一边把约束甩给 Z3——它的 incremental 模式是为这种”上百万次微调用”设计的
为什么 SMT-LIB benchmark 习惯把 Z3 当对照标尺——历史包袱：2008 之后的所有 SMT 求解器都被迫和它比

核心要点

Z3 是把 4 个层叠在一起的”洋葱”：

第 1 层：SAT 引擎（CDCL）

最里层是 minisat-2003 风格的 CDCL：VSIDS 选变量、watched literals 加速单元传播、conflict-driven 学习子句、restart 防卡死。这部分没新意，但 Z3 的实现细节优化（位级 packing、子句 GC 启发式）让它常年比通用 MiniSat 快 2-3 倍。

第 2 层：DPLL(T)——SAT 与 theory 的协作

按 nieuwenhuis-dpll-t-2006 的抽象规则：theory solver 提供 T-Propagate / T-Conflict / T-Learn 三个回调，挂在 SAT 引擎主循环里。每次 SAT 加一条文字，theory 立刻有机会喊”等等，矛盾”或”再加一条蕴含”。

第 3 层：多 theory 拼装（NO + MBTC）

Z3 同时跑线性算术、位向量、数组、未解释函数、datatype。要让它们”互相说话”，经典做法是 nelson-oppen-1979 的等式广播。但 NO 要求 theory stably-infinite——位向量天然违反（位宽固定→定义域有限）。

Z3 的招：model-based theory combination (MBTC)。每个 theory 不只回答”这两个变量等不等”，而是给出一个当前候选模型，框架根据模型猜哪些变量该相等，让 theory 验证。错了再撤。这绕过了 stably-infinite 限制，让 BV + LIA + 数组能同时跑。

第 4 层：量词 E-matching

SMT 一旦带 ∀x. P(x)，理论上半判定。Z3 用 e-graph（congruence closure 的图表示）做 E-matching：用户给”触发器”模式（trigger），引擎从 e-graph 找匹配的项，把量词实例化。这个跟”完备搜索”差很远，但在程序验证里 90% 的 VC 都能用 trigger 凑出来——务实工程派的胜利。

实践案例

案例 1：Dafny 一行 assert 怎么走到 Z3

Dafny 源码：

method Abs(x: int) returns (y: int)
  ensures y >= 0
{ if x < 0 { y := -x; } else { y := x; } }

编译器生成 verification condition：“对所有 x，存在执行路径让 y >= 0”。Boogie 把它翻成 SMT-LIB：

(declare-const x Int)
(declare-const y Int)
(assert (not (=> (or (and (< x 0) (= y (- x))) (and (>= x 0) (= y x))) (>= y 0))))
(check-sat)

Z3 跑 DPLL(T)，theory solver 是线性整数算术（LIA）。结果：unsat（即否定无解 → 原断言成立）。整个过程在零点几毫秒内完成。

案例 2：Z3 Python API 在 LLM 助手里的样子

from z3 import *
x, y = Ints('x y')
s = Solver()
s.add(x + y == 10, x > 3, y < 5)
print(s.check())  # sat
print(s.model())  # [y = 4, x = 6]

Lean Copilot / Aesop 之类的工具就是动态拼这种 SMT-LIB 字符串，喂给 Z3，拿回模型或 unsat core 反向引导证明搜索。

案例 3：Z3 与 chaff-2001 / minisat-2003 的关系

Chaff 是工业 CDCL 鼻祖（2001），MiniSat 是 600 行教学版（2003）。Z3 的 SAT 层吸收了两者的全部技巧：

从 Chaff 拿：VSIDS、watched literals、phase saving
从 MiniSat 拿：模块化 propagator 接口、incremental API 设计
自己加的：theory propagator 钩子（DPLL(T) 接入点）、e-graph 同步层

踩过的坑

Z3 不是”最聪明”的 SMT，是”最全能”的：CVC5 在某些 division（数据类型、字符串）超过 Z3；Bitwuzla 在纯位向量上更快。Z3 赢在覆盖面 + API 稳定 + 文档齐全。
量词不完备 → 同一个公式可能 sat 也可能 unknown：E-matching 找不到触发器实例化时返回 unknown。新手以为 Z3 出 bug，其实是问题本身半判定，需要补 :pattern 注解。
Python 绑定的语法陷阱：x + y == 10 在 Python 里因为 == 的歧义需要小心；混用原生 int 和 Z3 Int 时，类型推断常出错。官方建议显式用 IntVal(10)。
incremental 不是免费的：push/pop 看似便宜，但 theory state 复制有代价。验证工具频繁 push/pop 时，建议用 (push)/(pop) 局部小作用域，避免大包大揽。
proof object 默认关闭：(set-option :proof true) 会让 Z3 慢 5-10 倍并消耗大量内存。Lean / Coq 复演 Z3 证明时才开。

适用 vs 不适用场景

适用：

程序验证（Dafny / F* / Boogie / SPARK）
符号执行（KLEE / SymCC / angr）
自动定理证明的 SMT 后端（Lean / Coq / Isabelle 的 sledgehammer）
调度 / 配置 / 一阶约束求解
教学 SMT（API 友好 + Python binding 适合零基础）

不适用：

纯 SAT 大规模 → 用 minisat-2003 / Kissat 直接，绕开 SMT 包装
非线性实数算术规模大 → Z3 nlsat 慢，用 dReal / MathSAT
字符串密集 → CVC5 字符串 theory 更专
硬实时（毫秒级硬截止）→ SMT 搜索时间不可控
概率 / 模糊推理 → Z3 是经典逻辑

历史小故事（可跳过）

2002：de Moura 在 Stanford 做 SVC / CVC，写第一代 SMT
2006：Bjorner 与 de Moura 在 Microsoft Research 重组团队，决定从零写新 SMT
2007：Z3 0.1 内部用，验证 Windows 7 驱动模型 SLAM
2008 TACAS：本论文发表，2008 SMT-COMP 横扫
2012：Z3 在 GitHub 开源（MIT）；社区贡献涌入
2015 后：Lean / Dafny / F* / Move-Prover / TLA+ Apalache 全部把 Z3 当默认后端
2026：LLM 形式化（Lean Copilot / ProofNet / Aesop）几乎全用 Z3 当判定后端

学到什么

工程整合本身就是创新：Z3 没发明 DPLL(T)、没发明 NO、没发明 E-matching，但把三者拼到工业可用——这本身值一篇 TACAS。
API 决定生态：Z3 赢 CVC4/5 不是因为算法更强，是 Python 绑定 + push/pop + 模型/证明/core 三件套让下游工具用得顺手。
务实 > 完备：量词半判定 → 上 E-matching；NO 太严 → 上 MBTC。理论上不漂亮，但够用且能跑大问题。
基础设施有正反馈：Z3 一旦成默认，所有人就盯它的 bug 报告，文档越来越全，越来越难被替代——平台效应在 SMT 这种小圈子也成立。

关联

nieuwenhuis-dpll-t-2006 —— Z3 内核就是 DPLL(T) 抽象的工程实现
nelson-oppen-1979 —— Z3 用 NO 拼多 theory；MBTC 是其放宽版
minisat-2003 —— Z3 SAT 引擎设计参考
chaff-2001 —— Z3 SAT 层借的 VSIDS / watched literals 来自这里
hoare-logic —— 程序验证目标，VC 由 Z3 自动求解
clarke-cegar-2003 —— CEGAR 每轮调一次 Z3 检查不变式
fstar —— F* 依赖类型 + Z3 自动化
lean-prover —— Lean 4 的 decide / omega / polyrith 调 Z3

反向链接

acl2-2000 —— ACL2 — 用纯 Lisp 当数学对象，机器证明工业级硬件正确
boogie-2005 —— Boogie — 写一次验证后端，多种证明语言复用
chaff-2001 —— Chaff 2001 — 把 CDCL 工程化的两个杀手锏
clarke-cegar-2003 —— CEGAR — 用反例自动改进抽象，让大软件能被验证
dafny-2010 —— Dafny — 把”代码该满足的条件”直接写进语法，编译器自动证明
fstar —— F* — 把依赖类型、SMT 自动化、副作用追踪揉到一门语言里
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
hol-light-2009 —— HOL Light — 不到 500 行 OCaml 写出能证开普勒猜想的证明助手
hyperkernel-2017 —— Hyperkernel — 让 SMT 求解器一键验证操作系统内核
isabelle-hol-2002 —— Isabelle/HOL — 让程序证明像写数学论文一样可读
lean-prover —— Lean 4 — 用 Lean 重写的 Lean，让数学家和程序员共用一种语言
minisat-2003 —— MiniSat 2003 — 600 行 C++ 把 CDCL 写成教科书
nelson-oppen-1979 —— Nelson-Oppen 1979 — 让多个判定程序坐下来交换”我刚发现 a=b”
nieuwenhuis-dpll-t-2006 —— Nieuwenhuis-Oliveras-Tinelli 2006 — 给 SMT 求解器写一套数学规则书
vcc-2009 —— VCC — 给并发 C 加注解，让 SMT 自动证它对
why3-2013 —— Why3 — 写一次程序规范，多个证明器一起来证