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

待复核

是什么

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

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

这篇 TACAS 2008 论文的主贡献是工程整合（并带上 MBTC 等关键机制）：把 nieuwenhuis-dpll-t-2006 的 DPLL(T)、nelson-oppen-1979 的多 theory 协作、minisat-2003 的 SAT 引擎、e-graph 相等性闭包、量词 E-matching 塞进同一 C++ 内核，再加大量启发式。

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

为什么重要

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

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

核心要点

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

SAT 引擎（CDCL）：最里层像 minisat-2003——猜真假、撞墙就学教训、再猜。类比：填数独，填错一格就划掉整条推理链。Z3 的位级 packing、子句回收等实现细节，常让它在 SMT 场景下明显快于直接套 MiniSat。
DPLL(T)——SAT 与 theory 协作：按 nieuwenhuis-dpll-t-2006，算术/数组等”专家”（theory solver）挂在 SAT 主循环上。类比：主裁判猜布尔题，专家随时喊”矛盾”或”还能推出这条”。每次 SAT 加一条文字，theory 立刻有机会介入。
多 theory 拼装（NO + MBTC）：线性算术、位向量、数组要”互相说话”，经典是 nelson-oppen-1979 广播等式；但位向量定义域有限，不满足 NO 的无限域假设。Z3 用 MBTC：各 theory 先交候选模型，框架猜谁该相等再验证，错了撤回——让 BV + 整数 + 数组能同场跑。
量词 E-matching：带 ∀x. P(x) 时问题半判定。Z3 用 e-graph（把”相等的项”收成一团）做模式匹配：用户给触发器，引擎找匹配项再实例化。不完备，但程序验证里多数 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 四步走

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]

逐步解释：

Ints('x y')：声明两个整数变量
Solver() + add(...)：建求解器并塞进三条约束
check()：返回 sat（有解）或 unsat（无解）
model()：在 sat 时给出一组具体赋值（这里 x=6, y=4）

Lean Copilot 等工具就是动态拼这类约束，喂给 Z3，用模型或 unsat core 引导证明搜索。

案例 3：incremental push/pop（符号执行同款）

from z3 import *
x = Int('x')
s = Solver()
s.add(x > 0)
s.push()
s.add(x < 0)          # 临时加一条必矛盾的约束
print(s.check())      # unsat
s.pop()               # 撤掉临时约束
print(s.check())      # sat（只剩 x > 0）

逐步解释：push 开作用域 → 加路径约束 → check → pop 回退。KLEE / angr 每探索一条分支就这样微调用上百万次。

踩过的坑

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）：单次 VC 常在毫秒到秒级
符号执行（KLEE / SymCC / angr）：大量短生命周期 push/pop
证明助手的 SMT 后端（Isabelle sledgehammer、Lean 生态 SMT 插件）
调度 / 配置 / 一阶约束；教学 SMT（Python 绑定友好）

不适用：

纯 SAT 大规模 → 用 minisat-2003 / Kissat，绕开 SMT 包装
非线性实数规模大 → Z3 nlsat 慢，用 dReal / MathSAT
字符串密集 → CVC5 更专；硬实时毫秒截止 → 搜索时间不可控
概率 / 模糊推理 → 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 后：Dafny / F* / Move-Prover / TLA+ Apalache 等把 Z3 当默认后端；Lean 生态也常接 Z3
2026：LLM 形式化（Lean Copilot / ProofNet）常把 Z3 当判定后端

学到什么

工程整合本身就是创新：Z3 的主贡献是把 DPLL(T)/NO/E-matching 拼到工业可用，并带上 MBTC——这本身值一篇 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 生态里常见 SMT 插件/后端会调 Z3

反向链接

acl2-2000 —— ACL2 — 用纯 Lisp 当数学对象，机器证明工业级硬件正确
bohme-aflfast-2016 —— AFLFast — 把 fuzzing 的力气花在更少人走的路径上
boogie-2005 —— Boogie — 写一次验证后端，多种证明语言复用
cadar-klee-2008 —— KLEE — 用符号执行自动给复杂系统程序生成高覆盖测试
dafny-2010 —— Dafny — 把”代码该满足的条件”直接写进语法，编译器自动证明
driller-2016 —— Driller 2016 — 用符号执行给 fuzzing 打穿深分支
e-path-egraph —— E-Path — 把 CFG 优化从单行通道改成候选池
hoare-logic —— Hoare Logic — 把”程序对不对”变成”数学证明对不对”
hol-light-2009 —— HOL Light — 不到 500 行 OCaml 写出能证开普勒猜想的证明助手
hyperkernel-2017 —— Hyperkernel — 让 SMT 求解器一键验证操作系统内核
isabelle-hol-2002 —— Isabelle/HOL — 让程序证明像写数学论文一样可读
making-smart-contracts-smarter —— Making Smart Contracts Smarter — Oyente 用符号执行给智能合约找漏洞
vcc-2009 —— VCC — 给并发 C 加注解，让 SMT 自动证它对
why3-2013 —— Why3 — 写一次程序规范，多个证明器一起来证