可满足性模理论 (Satisfiability Modulo Theories)

很多实际问题用纯命题逻辑（SAT）表达时，要么根本无法表达。而用一般的一阶逻辑或高阶逻辑表达虽然自然，却无法自动高效求解。人们要么用专用算法解决特定问题（如线性规划、等价性检查），难以组合多种约束。SMT 把 SAT 的布尔搜索与多个理论求解器组合起来，使得混合理论约束可以被统一、自动地判定。

logic

SMT 的出现，本质上是为了解决一个核心矛盾：很多实际问题用纯命题逻辑（SAT）表达时，要么根本无法表达，要么表达后规模爆炸；而用一般的一阶逻辑或高阶逻辑表达虽然自然，却无法自动高效求解。

看一段再普通不过的代码：

void f(int x, int y) {
    int a[100] = {0};
    a[0] = 5;
    if (x + y > 10 && a[0] == 5) {
        // 目标分支
    }
}

假设 x、y 是来自外部的整数。我们想知道：有没有一组输入，能走进这个分支？

沿着这条路径，把进入分支需要满足的条件收集起来：

x + y > 10 \;\wedge\; a[0] = 5

问题于是变成：这组约束有没有解？

纯 SAT 求解器也能做，但你得先把 x、y 各拆成 32 个布尔变量，把加法展开成加法器电路，把数组展开成 100 个元素，最后交给它几千条子句。它只认识真假，不认识整数，也不认识数组。

SMT 求解器则直接读原式：x + y > 10 交给算术，a[0] = 5 交给数组。算术说取 x = 6, y = 5 就行，数组说 a[0] = 5 本来就成立。两边一对，返回 sat，并给出这组解。

同一个问题，一个要把语义拆成门电路，一个能直接利用语义。SMT 要做的，就是后者。

一、SMT 是什么

1.1 定义

把上面的过程抽象一下。SMT 是「SAT + 背景理论」：在某个理论 $T$ 规定的语义下，判定一个一阶逻辑公式是否存在满足它的赋值。

这里的关键词是「模理论」（modulo theories）。「模」可以理解为「相对于」：我们不再问公式在全部数学结构里是否成立，而是问它在某个特定理论——比如整数算术、位向量、数组——的解释下是否成立。

形式化一点，SMT 要回答的是：

\exists\, \sigma.\quad \sigma \models_T \varphi

也就是：是否存在一个赋值 $\sigma$ ，把每个变量映射到理论域里的值，使得 $\varphi$ 在这个理论的所有公理下为真。

回到开头的例子： $x + y > 10$ 是算术原子， $a[0] = 5$ 是数组原子，理论 $T$ 就是整数算术与数组的组合。SMT 要回答的，正是这组原子能不能同时为真。

1.2 公式的样子

SMT 公式由布尔结构和理论原子组成：

\varphi ::= \top \;\mid\; \bot \;\mid\; A \;\mid\; \neg\varphi \;\mid\; \varphi \wedge \varphi \;\mid\; \varphi \vee \varphi \;\mid\; \varphi \rightarrow \varphi

其中 $A$ 是理论原子，形如 $t_1 = t_2$ 、 $t_1 < t_2$ 、 $f(t_1) = t_2$ 、 $\mathrm{select}(a, i) = v$ 。原子内部的项由变量、常量和理论函数符号组成。

下面这个公式同时用到了三种理论：

\underbrace{(x + y > 10)}_{p}\;\wedge\;\underbrace{\bigl(a[0] = 5\bigr)}_{q}\;\wedge\;\bigl(\underbrace{f(x) \ne f(y)}_{r} \vee\, y \le 0\bigr)

$x + y > 10$ 属于线性整数算术：它知道 $+$ 是加法、 $>$ 是全序；
$a[0] = 5$ 属于数组理论：它知道 select 和 store 的读写语义；
$f(x) \ne f(y)$ 属于未解释函数：它不知道 $f$ 具体算什么，只知道「同一个输入必须得到同一个输出」。

对 SAT 来说，这三个原子只是三个裸的布尔变量 $p, q, r$ 。对 SMT 来说，它们各自带着一整套内部结构。

这张图就是 SMT 的骨架：布尔层负责「怎么组合」，理论层负责「每个原子是什么意思」。

1.3 背景理论

SMT 里常用的理论有这么几类：

EUF（QF_UF）：只处理相等和未解释函数，适合描述对象相等、指针别名。
线性算术（QF_LRA / QF_LIA）：处理 $+$ 、 $\le$ 和常数；实数版是 QF_LRA，整数版是 QF_LIA。
非线性算术（QF_NRA / QF_NIA）：允许乘法；实数版可判定，整数版不可判定。
位向量（QF_BV）：描述机器整数和硬件电路，加法是模 $2^n$ 的。
数组（QF_AX / QF_AUFBV）：用 select 和 store 描述内存读写。
浮点（QF_FP）：描述 IEEE 754 浮点运算。
字符串：描述 concat、contains 等操作，工业实现常常不完整。

QF 是 quantifier-free 的缩写，意思是「无量词」。绝大多数 SMT 求解器面对的都是这个片段。

可以把 SAT 看成 SMT 的一个特例：当理论 $T$ 为空、所有原子都是裸命题时，SMT 就退化成 SAT。

反过来，SMT 也可以看成 SAT 的一次「语义升级」：布尔骨架不变，但每个命题不再是黑盒，而是有内部结构、可以被理论求解器检查和反驳的对象。

这个升级带来的好处，要放到具体的历史困境里才看得清楚。

二、SMT 之前

2.1 位爆破

SAT 只认布尔变量。要用它处理整数，标准做法叫位爆破（bit-blasting）：把整数拆成一个个布尔变量，再把算术运算展开成逻辑门电路，最后用 Tseitin 变换把电路转成 CNF 子句。

看一个具体的小例子。取两个 4 位无符号整数 $x, y$ ，约束是：

x + y = 10 \;\wedge\; x > y

SAT 看到的是 8 个布尔变量 $x_3 x_2 x_1 x_0$ 和 $y_3 y_2 y_1 y_0$ 。为了表达加法，需要 4 个全加器。每个全加器有三个输入 $a, b, c_{in}$ 、两个输出 $s, c_{out}$ ，满足：

s = a \oplus b \oplus c_{in}, \qquad c_{out} = (a \wedge b) \vee \bigl(c_{in} \wedge (a \oplus b)\bigr)

把这两个等式转成 CNF，一个全加器大约 17 条子句。4 位加法器就是 4 个全加器，约 70 条子句。再加上「和等于 1010、进位为 0」的 5 条单元子句，以及一个 4 位比较器的几十条子句，整个约束变成一百多条子句、几十个辅助变量。

而原始约束只有一行：

x + y == 10 && x > y

求解器可能给出 $x = 0110$ 、 $y = 0100$ ，但它并不知道这是 6 和 4。它只知道这一组真假值恰好让所有子句为真。

规模还不是最麻烦的，语义丢失才是。假设我们想证明 $x + y = y + x$ 。在算术里这是一条公理，一秒都不用。但在 SAT 里，左边是一个「先加 $x$ 再加 $y$ 」的电路，右边是一个「先加 $y$ 再加 $x$ 」的电路，两个电路内部结构不同，SAT 只能把两边都展开，再逐位证明输出相等。它不知道「加法可交换」，只知道一堆门。

打个比方：这就像为了判断一首诗是否押韵，先把它拆成一个个字母，再让机器从字母的排列里重新发现什么是韵脚。信息没有丢，但结构没了。

2.2 不可判定

那干脆用表达力最强的一阶逻辑，让自动定理证明器去证，不行吗？

不行。看一个具体方程：

x^3 + y^3 + z^3 = 33

它看起来很简单。它有整数解，一个已知解是：

\begin{aligned} 33 ={}& 8866128975287528^3 \\ &+ (-8778405442862239)^3 \\ &+ (-2736111468807040)^3 \end{aligned}

这三个数都是 16 位数，直到 2019 年才被找到。如果把 $x, y, z$ 都编码成 64 位整数，搜索空间是 $2^{192}$ ；按每秒试十亿个赋值来算，也要 $10^{41}$ 年量级。位爆破在这里基本不可行。

更根本的是，这不是「这一个方程特别难」的问题。希尔伯特第十问题问的是「是否存在算法判定整系数多项式方程有没有整数解」，这个问题在 1970 年被马蒂亚谢维奇证明为否。证明的思路很巧妙：任给一台图灵机和一段输入，都能构造出一个整系数多项式方程，使方程有解当且仅当图灵机停机。既然停机问题不可判定，一般的方程判定问题也不可判定。换句话说，想写一个能判定所有这类方程的通用算法，这件事本身就是不可能的。

工程上的后果很直接：自动定理证明器可能跑了一整天，最后告诉你「我不知道」。对于一个需要每秒判定成千上万条路径条件的程序分析工具来说，这是不可接受的。

2.3 难以组合

另一条路是「一个问题配一个专用算法」：线性规划用单纯形法，只懂实数线性约束；并查集只懂「相等」；BDD 只懂布尔函数；自动机只懂正则语言和字符串匹配。

这些算法在各自领域都很好用，但真实的程序约束往往是混合的。看一个只有两个原子的例子：

x = y \;\wedge\; f(x) \ne f(y)

假设我们分别去问两个求解器：

算术求解器只看 $x = y$ ，回答 sat，比如 $x = y = 0$ ；
EUF 求解器只看 $f(x) \ne f(y)$ ，也回答 sat：它把 $x, y$ 当成两个不同的常量，令 $f(x) = 0$ 、 $f(y) = 1$ 。

如果把两个答案一拼，说「两边都可满足，所以整体可满足」，就错了。因为 $x = y$ 意味着 $f(x)$ 必须等于 $f(y)$ ，与 $f(x) \ne f(y)$ 直接矛盾。整体其实是 unsat。

要得到正确答案，两个求解器必须交换信息：算术把等式 $x = y$ 告诉 EUF，EUF 立刻推出 $f(x) = f(y)$ ，冲突。谁来负责交换？交换哪些事实？什么时候交换？在 SMT 之前，这些都是需要人工设计的事情。

数组和算术之间也有同样的坑。i = j ∧ a[i] ≠ a[j] 单独看两边都可满足，合起来却不可满足，因为下标相等就意味着读到的值相等。没有任何一个专用算法能独自看出这一点。

2.4 门槛太高

还有一条路是 Coq、Isabelle、ACL2 这类交互式定理证明器。它们的表达力极强，能处理带量词、带归纳的复杂性质，但代价是需要人写证明脚本。

比如在 Coq 里证明「任何自然数加零都等于它自己」，要写：

Theorem plus_0_r : forall n : nat, n + 0 = n.
Proof.
  induction n as [| n' IH].
  - simpl. reflexivity.
  - simpl. rewrite IH. reflexivity.
Qed.

这几行不是装饰：

induction n 把目标拆成两种情况： $n = 0$ 和 $n = S(n')$ ；
第一种情况，simpl 把 $0 + 0$ 化简成 $0$ ，reflexivity 确认两边相等；
第二种情况，simpl 把 $S(n') + 0$ 化成 $S(n' + 0)$ ，再用归纳假设 IH 把 $n' + 0$ 换成 $n'$ ，最后 reflexivity 收尾。

每一步往哪走、用哪条归纳假设，都是人选的。这还只是自然数加零。真实的程序验证要证循环不变式、数组不变式、指针分离，脚本可能几百上千行。

程序分析场景里，工具每秒要生成并判定几千条路径条件。不可能每条都停下来等工程师写一段证明。自动化程度不够，就无法工业部署。

2.5 小结

几条路，各有各的难处：

纯 SAT 快，但把高层语义压成门电路之后，规模爆炸、语义丢失；
一阶逻辑表达力强，但一般情形不可判定，自动证明器可能永远给不出答案；
专用算法在自己的理论里很好用，碰到混合约束就各自为政；
交互式定理证明能处理复杂性质，但每条路径都等人写脚本，工业化无从谈起。

SMT 要做的，就是在这几条路的夹缝里找一个中间地带：表达力足够描述程序，判定过程保证自动，还能把多个理论组合起来。

三、SMT 的解法

3.1 收缩片段

SMT 的第一个策略是主动放弃一部分表达力，只保留可判定的片段。

具体做法是：把主战场放在无量词片段，只允许特定理论的组合。这样既避开了 2.2 节里的不可判定性，又保留了描述程序行为所需的大部分能力。

为什么可以放弃量词？因为程序分析产生的验证条件，大多数天然就是无量词的。符号执行收集到的路径条件，是对「这一条路径上各个变量的具体取值」的约束，不需要「对所有 $i$ ， $a[i] > 0$ 」这种全称陈述。

需要量词的地方——循环不变式、数组的整体性质、归纳证明——通常由上层工具负责：抽象解释负责生成不变式， $k$ -induction 负责把归纳化归为有限次查询，SMT 只作为底层的判定引擎。这是一个分工，而不是缺陷。

当然，「可判定」不等于「容易」。QF_UF、QF_LIA、QF_BV 都是 NP-complete；QF_LRA 是多项式时间；QF_NRA 可判定，但最坏情况是双指数；QF_NIA 则直接不可判定。

SMT 在选定的片段内保证了「答案一定会来」，但不保证「答案来得快」。工程上的成败，很大程度上取决于启发式和问题编码。

3.2 直接表达

第二个策略是让公式直接说人话。

同样是「 $x + y > 10$ 且 $a[0] = 5$ 」，SMT 不需要把 $x, y$ 拆成 64 个布尔变量，也不需要把数组展开成 100 个元素。它把这两个条件原样保留为两个理论原子，交给对应的求解器。

关键在于「按需展开」：

算术：直接用单纯形法或分支定界，在整数/实数域上推理，完全不经过布尔编码。
数组：用 read-over-write 公理，只在公式里真的出现某个下标时才实例化。
位向量：这一条要诚实一点——大多数求解器内部仍然会做位爆破，因为位级编码对硬件电路太有效了。但这件事发生在求解器内部，只针对相关子表达式，而且会配合字级重写（比如 $x \,\&\, 0 = 0$ 、 $x - x = 0$ ）和等价类合并。对使用者来说，它仍然是透明的。

数组的 read-over-write 公理长这样：

\mathrm{select}\bigl(\mathrm{store}(a, i, v), j\bigr) = \begin{cases} v, & i = j \\ \mathrm{select}(a, j), & i \ne j \end{cases}

如果公式里只关心 $a[0]$ ，求解器就只实例化 $i = 0$ 这一条，剩下的 99 个元素根本不会出现。这是「按需」和「全局」的区别，也是 SMT 能在数组上跑赢位爆破的原因。

所以更准确的说法不是「SMT 消灭了底层编码」，而是：SMT 把「怎么编码」的决定权从用户手里交给了求解器。求解器可以根据理论特性选择最合适的内部表示，而不是让用户先做一次不可逆的全局展开。

用同一个约束对比一下。纯 SAT 的版本要生成数百到上千个布尔变量、上千条子句；SMT 的版本只保留两个理论原子。SAT 只能做布尔剪枝，SMT 能利用算术和数组的语义；SAT 的答案是一组布尔赋值，还要反解出 $x, y$ ，SMT 直接给出 $x = 6, y = 5$ 。

3.3 组合理论

第三个策略是让不同理论通过共享等式来协作。

最经典的方法是 Nelson–Oppen 组合。它的前提是：两个理论的签名不相交（各自管各自的符号），并且都满足「稳定无限」性质（任何可满足的公式都有无穷模型）。在这个前提下，两个理论只需要交换变量之间的等式，就能组合成一个完整的判定过程。

看一个例子：

x = y \;\wedge\; f(x) \ne f(y)

算术部分看到 $x = y$ ，本身没有矛盾；
EUF 部分如果不知道 $x = y$ ，就会认为 $f(x)$ 和 $f(y)$ 可以不同，也不会报错；
一旦算术把等式 $x = y$ 传给 EUF，EUF 立刻推出 $f(x) = f(y)$ ，与 $f(x) \ne f(y)$ 冲突。

于是整个公式被判为不可满足。这个结论不是某一个理论单独得出的，而是两个理论「对了一下账」才对出来的。

再看一个反方向的例子：

x + y > 10 \;\wedge\; x = 3 \;\wedge\; y = 4

这里算术部分自己就能算出 $3 + 4 = 7 < 10$ ，直接判 unsat，根本不需要 EUF 参与。

现代求解器（Z3、cvc5 等）通常不严格照搬经典 Nelson–Oppen，而是在 DPLL(T) 框架下做「理论传播 + 冲突解释」。但核心思想没变：每个理论只懂自己那一摊，通过交换少量关键事实来达成全局一致。

有一个细节值得注意：如果理论是「非凸」的，光交换等式还不够。比如在整数算术里， $x \ne 0$ 等价于 $x \le -1 \vee x \ge 1$ ，这是一个析取，没法用一组等式表达。上层只能做情况分裂（case split），分别假设每一支再检查。这会让组合复杂度上升，也是混合理论求解有时会突然变慢的原因之一。

3.4 给出解释

第四个策略是不只回答是或否，还给出可操作的结果。

sat：求解器返回一个模型，给出每个变量的具体取值。对符号执行来说，这就是一条能触发目标路径的测试输入。
unsat：求解器可以返回一个 unsat core，也就是一组不可满足的子约束，告诉你「是这几条打架了」。
插值：从 $A \Rightarrow B$ 的不可满足性中提取一个只含共同变量的中间公式（Craig interpolant），用于程序验证中的不变式合成和抽象精化。
证明：部分求解器能输出 resolution 证明，供独立检查，避免「求解器说有漏洞，但你不知道为什么」的黑盒困境。

这一点经常被忽略，但它决定了 SMT 能不能真正嵌进工具链。一个只会输出 unsat 的求解器，在调试时几乎没用；一个能告诉你「第 3、7、9 条约束冲突」的求解器，才能帮工程师定位问题。

3.5 增量求解

第五个策略是增量求解（incremental solving）。

符号执行的路径是一棵树：父路径的约束是子路径约束的前缀。如果每换一条路径都从头求解，大量工作会被重复浪费。

SMT-LIB 提供了 push / pop 和 check-sat-assuming，允许在已有约束的基础上临时加入假设、求解、再回退。求解器会保留之前学到的子句和理论状态。一条路径判 unsat 后回退到分叉点，下一条路径可以接着用。

KLEE、angr 这类工具都重度依赖这个特性。没有增量求解，符号执行的性能会差一个数量级。

四、DPLL(T)

4.1 总体架构

现代 SMT 求解器的标准架构叫 DPLL(T)，更准确的名字是 CDCL(T)：外层是带冲突学习的 SAT 求解器，内层挂一个或多个理论求解器。

用一句话概括这个循环：

把公式里的每个理论原子替换成一个命题变量，得到一个纯布尔公式；
让 SAT 求解器找一个布尔模型；
把布尔模型翻译回理论原子的真假，交给理论求解器检查；
如果理论层说「一致」，就得到 sat 和模型；
如果理论层说「冲突」，就把冲突总结成一条新的布尔子句，塞回 SAT 层，让它换个方向再搜；
如果 SAT 层把所有可能性都穷尽了，就得到 unsat。

可以把它想象成一个总承包商和几个专业工种的协作：总承包商（SAT）负责排期和组合，电工、水管工（理论求解器）负责检查自己那部分是否可行。电工说「这个排期下电线会短路」，总承包商就把这条经验记下来，换一个排期重新试。

4.2 布尔抽象

布尔抽象（也叫 propositional abstraction）是两层之间的接口。

以这个公式为例：

\varphi = (x > 0 \vee y > 0) \;\wedge\; (x + y < 0)

引入三个命题变量：

p \equiv (x > 0), \qquad q \equiv (y > 0), \qquad r \equiv (x + y < 0)

布尔骨架变成：

(p \vee q) \;\wedge\; r

SAT 求解器在这个骨架上的搜索空间只有 $2^3 = 8$ 种赋值。它先试 $p = \top, q = \top, r = \top$ ，把这三个真值交回理论层。

理论层看到的是三个文字（literal）：

x > 0, \qquad y > 0, \qquad x + y < 0

线性算术求解器立刻发现：前两个推出 $x + y > 0$ ，与第三个矛盾。这是一次理论冲突。

注意，理论层收到的不是「原子为真」，而是「带正负号的文字」。 $q = \bot$ 对应的是 $\neg(y > 0)$ ，也就是 $y \le 0$ 。理论求解器必须能处理这种否定形式，这也是为什么它通常直接操作形如 $t_1 \le t_2$ 的不等式，而不是只处理等式。

4.3 CDCL

SAT 层用的是 CDCL（冲突驱动子句学习）。它的核心循环大致如下：

loop:
    conflict = unit_propagate()      # 单元传播
    if conflict:
        if decision_level == 0: return UNSAT
        lemma = analyze(conflict)    # 冲突分析
        backtrack()                  # 非时序回跳
        add_clause(lemma)            # 学习子句
    else:
        if all_variables_assigned(): return SAT
        decide()                     # 选一个未赋值的变量

三个关键机制：

单元传播：一条子句里只剩一个未赋值的文字时，强制它取能让子句为真的值。
冲突分析：从冲突出发，反向找出是哪几个决策导致的，生成一条新的子句。这条子句是原公式的逻辑推论，加进去不会改变解集。
非时序回跳：不退回上一层，而是直接跳回冲突的真正源头，跳过大量无用的搜索。

CDCL 是过去二十年 SAT 求解器性能提升的主要来源。SMT 做的事情，基本上是把这套成熟的工程能力「复用」到理论层。

4.4 理论求解器

理论层要做的事情叫 T-一致性检查：给定一组带正负号的原子，判断它们在理论 $T$ 下是否可能同时为真。

不同理论有不同的算法。

EUF

EUF（Equality with Uninterpreted Functions）只关心相等关系和函数的一致性。核心是两件事：

用并查集维护变量的等价类；
用同余闭包（congruence closure）保证：如果 $a = b$ ，那么 $f(a) = f(b)$ 。

例子：

a = b \;\wedge\; b = c \;\wedge\; f(a) \ne f(c)

并查集把 $a, b, c$ 合并成一个类；同余闭包发现 $f(a)$ 和 $f(c)$ 的参数相等，于是把 $f(a), f(c)$ 也合并；但公式又要求它们不等，冲突，判 unsat。

EUF 在程序分析里非常有用，因为指针别名、对象身份、类型相等，本质上都是「未解释函数的相等性」。

线性算术

QF_LRA 用单纯形法（更准确地说，是 SMT 里常用的 general simplex）。它先维护一组满足所有等式的赋值，再通过枢轴变换（pivot）调整变量的取值，直到所有上下界约束也被满足；如果怎么调都满足不了，就报告冲突。

QF_LIA 在此基础上加分支定界：先按实数求解，如果解里某个整数变量取了小数，就分裂成两支，比如 $x \le \lfloor v \rfloor$ 和 $x \ge \lceil v \rceil$ ，分别再解。

例子：

3x + 2y = 5, \qquad x, y \ge 0, \qquad x, y \in \mathbb{Z}

实数松弛下， $x = 5/3, y = 0$ 是一个解，但 $x$ 不是整数。分支：

假设 $x \le 1$ ： $x$ 只能取 $0$ 或 $1$ ； $x = 0$ 时 $y = 2.5$ 仍不是整数， $x = 1$ 时 $y = 1$ ，得到整数解，sat；
另一支 $x \ge 2$ 就无须再看了。

如果两支都不可行，就判 unsat。实际求解器还会加上割平面（cut）和更强的预处理，避免分支树爆炸。

位向量

QF_BV 最常用的方法还是位爆破：把位向量运算展开成门电路，再交给 SAT 层。但因为位向量有固定宽度，这种展开是有限且可预测的。

现代求解器会先做字级重写，把明显恒真的部分消掉，比如：

x \,\&\, 0 = 0, \qquad x - x = 0, \qquad x \ll 0 = x

然后再决定哪些子表达式值得展开。乘法是位向量的难点，因为乘法器电路规模大，求解器通常会配合专门的乘法推理和等价类传播。

位向量的语义是模运算，这一点非常重要：

x + 1 \equiv 0 \pmod{2^{32}} \;\wedge\; x \ne \texttt{0xFFFFFFFF}

在 32 位无符号整数里，唯一满足 $x + 1 \equiv 0$ 的值就是 0xFFFFFFFF，所以这个公式是 unsat。如果把它当成数学整数， $x = -1$ 又不等于 0xFFFFFFFF，结论就完全不同。选错理论，漏洞检测就会漏报或误报。

数组

数组理论的核心是 select 和 store 两条操作，以及前面提到的 read-over-write 公理。

求解器不会一次性展开所有下标，而是采用惰性公理实例化（lazy axiom instantiation）：先假设数组是一致的，当检查中发现某个 select(store(...)) 需要用到公理时，才生成对应的引理加入公式。这叫「按需生成」，也叫 lemma-on-demand。

例子：

\mathrm{select}\bigl(\mathrm{store}(a, i, v), j\bigr) = w \;\wedge\; i = j \;\wedge\; w \ne v

由 $i = j$ 和 read-over-write 公理，左边等于 $v$ ；于是 $v = w$ ，与 $w \ne v$ 冲突，unsat。整个过程中，数组的长度、其他下标的值，全都不需要知道。

其他理论

字符串理论通常用自动机或序列理论处理，word equation 本身可判定，但加上长度约束、正则约束后很多片段会变得不可判定，工业求解器往往采用不完整但实用的策略。浮点理论通常把 IEEE 754 的位级语义编码成位向量，再交给 QF_BV 后端。

4.5 冲突学习

理论冲突不会只让当前搜索失败一次，它会变成一条理论引理（theory lemma），永久加入布尔公式。

前面 4.2 节的例子：

x > 0, \qquad y > 0, \qquad x + y < 0

这三条文字不可同时为真，所以下面这条子句是理论有效的：

\neg(x > 0) \;\vee\; \neg(y > 0) \;\vee\; \neg(x + y < 0)

把它翻译回命题变量，就是：

\neg p \;\vee\; \neg q \;\vee\; \neg r

SAT 层学到这条子句之后，就再也不会同时选 $p, q, r$ 都为真了。这一步是 DPLL(T) 效率的关键：理论层的「一次性检查」变成了布尔层的「永久知识」。

如果没有冲突学习，SAT 层会在同一个理论冲突上反复撞墙；有了它，搜索空间被真正地剪掉了。

4.6 完整例子

还是用这个公式：

\varphi = (x > 0 \vee y > 0) \;\wedge\; (x + y < 0)

第 1 轮：SAT 层选择 $p = \top, q = \top, r = \top$ 。理论层检查 $\{x > 0,\ y > 0,\ x + y < 0\}$ ，发现 $x + y > 0$ ，冲突。生成引理 $\neg p \vee \neg q \vee \neg r$ 并回跳。

第 2 轮：SAT 层在引理约束下重新搜索，可能选择 $p = \top, q = \bot, r = \top$ 。理论层检查：

x > 0, \qquad y \le 0, \qquad x + y < 0

取 $x = 1, y = -2$ ，三条同时成立。理论层返回一致，求解器输出：

\textbf{sat}, \qquad x = 1,\ y = -2

这就是一个完整的 DPLL(T) 循环：一次冲突、一次学习、一次成功。

在真实求解器里，理论层还会做理论传播：不等 SAT 层给出完整赋值，就提前推出某些文字必须为真或为假，从而更早剪枝。这让循环通常只需要很少几轮。

理论正确不代表跑得快。工业级求解器还依赖大量工程优化：

预处理：化简公式、消除冗余变量、把公式规范化成求解器偏好的形式。
理论传播：理论层主动推导文字，而不是被动等待完整赋值。
重启策略：按 Luby 序列或指数策略重启，避免陷入坏的搜索区域。
子句删除：学习子句太多会拖慢传播，需要定期清理。
多引擎组合：同一个问题用不同策略并行求解（portfolio），谁先出结果用谁。
专用推理：针对乘法、数组、字符串等难点，加入专门的推理规则。

4.7 复杂度边界

必须强调：可判定不等于可解。

SAT 是 NP-complete；
QF_BV、QF_LIA、QF_UF 也都是 NP-complete；
QF_LRA 虽然是多项式时间，但实际常数很大；
QF_NRA 可判定，但最坏情况是双指数；
QF_NIA 直接不可判定。

这意味着，工业问题的最坏情况仍然是指数级的。求解器的成功，很大程度上依赖问题结构、编码方式和启发式。遇到超时，工具通常只能返回「未知」，而不是「安全」。

这也是为什么实际系统里，SMT 很少单独使用，而是和抽象解释、fuzzing、测试生成等方法组合。

五、漏洞检测

5.1 问题转化

软件漏洞检测的核心问题可以写成一句话：

是否存在一个输入，让程序走到某个危险位置，并且违反某条安全性质？

形式化之后，它就是一个存在性查询：

\exists\, \mathit{input}.\quad \underbrace{\mathrm{PC}(\mathit{input})}_{\text{路径条件}} \;\wedge\; \underbrace{\mathrm{Violate}(\mathit{input})}_{\text{安全性质取反}}

$\mathrm{PC}$ 是路径条件，描述「走到这里需要满足哪些约束」；
$\mathrm{Violate}$ 是安全性质的否定，描述「怎样才算越界/溢出/空指针解引用」。

如果这个公式 sat，求解器给出的模型就是一条能触发漏洞的输入，漏洞可达；如果 unsat，说明在这条路径上不可能违反性质，可以安全剪枝。

这个转化是整个应用的基石：「找漏洞」变成了「解约束」。

5.2 缓冲区溢出

先看一个最直观的例子：

void process(char *input, int len) {
    char buf[8];
    if (len > 4 && len < 12) {
        memcpy(buf, input, len);   // 可疑点
    }
}

buf 只有 8 字节，而 memcpy 拷贝 len 字节。如果 len 能大于 8，就会发生栈溢出。

符号执行引擎把 input 和 len 当作符号变量，沿路径走到 memcpy 时，收集到的路径条件是：

len > 4 \;\wedge\; len < 12

要判断溢出是否可达，就在路径条件上再加一条「写入长度超过缓冲区大小」：

len > 4 \;\wedge\; len < 12 \;\wedge\; len > 8

写成 SMT-LIB：

(set-logic QF_LIA)
(declare-const len Int)
(assert (and (> len 4) (< len 12) (> len 8)))
(check-sat)
(get-model)

求解器返回：

sat
(model
  (define-fun len () Int
    9)
)

len = 9 是一个合法解：它满足 $4 < 9 < 12$ ，同时 $9 > 8$ 。这条路径可达，memcpy 会往 8 字节的缓冲区里写 9 字节，溢出 1 字节。是否真的覆盖到返回地址取决于栈布局，但「越界写」这个事实本身已经成立。

如果把代码改成：

if (len > 4 && len <= 8) {
    memcpy(buf, input, len);
}

约束就变成：

len > 4 \;\wedge\; len \le 8 \;\wedge\; len > 8

求解器返回 unsat。这条溢出路径不可达，工具不会报告漏洞。

注意这里用的是 QF_LIA（整数线性算术）。真实的 C 代码里 len 是 32 位 int，更精确的建模应该用 QF_BV：

(set-logic QF_BV)
(declare-const len (_ BitVec 32))
(assert (and (bvsgt len (_ bv4 32))
             (bvslt len (_ bv12 32))
             (bvsgt len (_ bv8 32))))
(check-sat)
(get-model)

注意这里用的是有符号比较（bvsgt / bvslt），因为 C 里的 int 是有符号的。一个可能的模型是 len = #x00000009。对这个例子来说，两种建模的结论一样；但下一个例子就会看到，理论选错，结论可能完全相反。

5.3 整数溢出

void copy(char *src, unsigned int off, unsigned int len) {
    char buf[64];
    if (off + len <= 64) {
        memcpy(buf + off, src, len);
    }
}

看起来检查很严：只有 off + len 不超过 64 才拷贝。但 off 和 len 都是 32 位无符号整数，加法是模 $2^{32}$ 的。

攻击者可以取：

\text{off} = \texttt{0xFFFFFFF0}, \qquad \text{len} = \texttt{0x20}

计算一下：

\begin{aligned} \text{off} + \text{len} &= \texttt{0xFFFFFFF0} + \texttt{0x20} \\ &= \texttt{0x100000010} \\ &\equiv \texttt{0x10} = 16 \pmod{2^{32}} \end{aligned}

$16 \le 64$ ，检查通过。但 buf + off 指向的是缓冲区外大约 4GB 的位置，memcpy 会往一个完全无关的地址写 32 字节。这是一个典型的整数溢出导致的任意地址写。

用位向量理论来问：

(set-logic QF_BV)
(declare-const off (_ BitVec 32))
(declare-const len (_ BitVec 32))
(assert (bvule (bvadd off len) (_ bv64 32)))
(assert (bvugt off (_ bv64 32)))
(assert (bvule len (_ bv64 32)))
(check-sat)
(get-model)

求解器返回 sat，模型可能是：

off = #xfffffff0
len = #x00000020

漏洞可达。

如果换一种建模，把 off 和 len 当成数学整数：

\text{off} + \text{len} \le 64 \;\wedge\; \text{off} > 64 \;\wedge\; \text{len} \ge 0

这个公式是 unsat，因为 $\text{off} + \text{len} > 64$ 直接和第一条矛盾。工具会得出结论「没有漏洞」，而实际上漏洞就在那里。

同一个程序，两种理论，两个相反的答案。 这就是为什么漏洞检测工具必须精确建模目标语言的整数语义：C 的 unsigned int 是模运算，不是数学整数。

5.4 空指针

静态分析经常报「可能的空指针解引用」。这类告警里有很多是误报，SMT 可以用来过滤。

int read_flag(struct node *p) {
    if (p == NULL) return 0;
    return p->flag;     // 静态分析：p 可能为空？
}

工具在 p->flag 处收集路径条件。走到这一行，必然经过了 p == NULL 为假的分支，所以路径条件里包含：

p \ne \texttt{NULL}

静态分析如果只做局部启发式，可能会说「p 可能是空指针」。这时问 SMT：

p = \texttt{NULL} \;\wedge\; p \ne \texttt{NULL}

这是明显的矛盾，返回 unsat，告警被排除。

反过来，如果代码是：

int read_flag(struct node *p) {
    if (p->flag == 1) {   // 这里没有检查 p
        return 1;
    }
    return 0;
}

路径条件里没有 $p \ne \texttt{NULL}$ ，查询：

p = \texttt{NULL}

返回 sat，模型给出 p = NULL。这是一条真实可达的空指针路径，告警保留。

这个用法体现了一个重要原则：SMT 不负责发现漏洞，它负责判断「这条路径到底可不可能」。发现可疑点靠前端分析，排除误报靠 SMT。

5.5 数组越界

int get(int *a, int i) {
    if (i < 100) {
        return a[i];     // i 可能为负
    }
    return -1;
}

只检查了上界，没检查下界。问 SMT：

i < 100 \;\wedge\; i < 0

返回 sat，例如 i = -1。a[-1] 是一次越界读。

如果加上下界检查：

if (i >= 0 && i < 100) {
    return a[i];
}

约束变成：

i \ge 0 \;\wedge\; i < 100 \;\wedge\; i < 0

返回 unsat，越界路径被排除。

这个例子还可以扩展成带数组理论的版本。比如要验证「下标不同时，写入 a[j] 不会影响对 a[i] 的读取」，可以把「影响了」写成公式，再问它是否可满足：

i \ne j \;\wedge\; \mathrm{select}\bigl(\mathrm{store}(a, j, v), i\bigr) \ne \mathrm{select}(a, i)

数组理论会展开 read-over-write 公理，算术理论会处理 $i \ne j$ ，两个理论协作给出 unsat——也就是说，「写入影响了另一个下标」的情况不可能发生。这正是 3.3 节里理论组合的实际用武之地。

5.6 完整流程

把上面的步骤串起来，一个典型的漏洞检测流程是这样的：

整个系统里，SMT 只负责中间那个方框。前面「怎么把程序变成公式」是符号执行引擎的事，后面「怎么确认漏洞」是测试和人工的事。公式建得对不对，直接决定 SMT 的结论有没有意义。

所以，SMT 在漏洞检测里的正确定位是：一个强大但需要被正确使用的判定引擎。它能把「这条路径可不可能」回答得很准，但「该问哪些问题」「怎么把程序翻译成问题」，仍然依赖前端工具和工程师的判断。

六、小结

回到开头那道小学题。SMT 的价值，不是把 $x > 3 \wedge x < 5$ 算得更快，而是让机器在保留「整数」「数组」「位向量」这些概念的前提下，仍然能自动地回答「有没有解」。

SMT = SAT + 背景理论。 布尔层负责组合，理论层负责语义，两者通过「原子真值」这一层接口通信。 它的核心取舍是用表达力换可判定性。 把主战场放在无量词的可判定片段，换来一个在片段内保证终止、且能处理工业规模混合约束的自动判定过程。