Satisfiability Modulo Theories（可满足性模理论）

SMT（Satisfiability Modulo Theories）求解器是一类用于判断逻辑公式在“某个或某些背景理论”下是否可满足的自动化工具，它将经典的布尔可满足性（SAT）推广到包含整数、实数、位矢量、数组、字符串、以及其他数据结构的更丰富逻辑中。SMT 求解器的目标是：给定一个第一阶逻辑公式，判断是否存在一组变量赋值，使该公式在所选理论（如线性算术、位矢量、不解释函数等）下成立；如果可行还可生成具体模型（赋值）以供下游工具或用户分析。
相比纯粹的 SAT 问题，SMT 问题中的字面量（atoms）不仅仅是布尔变量，而是更复杂的谓词（如 x + y > 0、select(A, i) = v、length(s) < 10 等），因此 SMT 求解器需要结合布尔搜索和理论决策过程来协同工作。

历史与发展

SMT 领域起源于 20 世纪 70—80 年代，用于形式化方法与自动定理证明中引入决策过程的早期工作，包括 Nelson–Oppen 方法、Shostak 方法，以及 Boyer–Moore 定理证明器中的算术决策过程等 people.eecs.berkeley.edu 维基百科。2000 年代中期，Nieuwenhuis 等人在 DPLL(T) 框架中正式将 SAT 求解器与可组合理论求解器耦合，奠定了现代 SMT 求解器的核心架构维基百科 resources.mpi-inf.mpg.de。
随着 SMT-COMP（SMT Solver Competition，自 2005 年起举办）的推动，以及工业界对程序验证、硬件验证、符号执行等领域需求的增长，SMT 求解器在性能与功能上经历了飞速迭代，涌现出 Z3、CVC4/CVC5、Yices、MathSAT、Bitwuzla、OpenSMT 等多款工具。

简单例子

假设有这样一段 LLVM IR 优化前（source）和优化后（target）代码：
; source %res1 = add i32 %x, %y ; target %res2 = add i32 %y, %x
我们要验证：对任意 32 位整型输入 x、y，两段代码的输出总是相等。
流程为：

解析 IR
Alive2 读入 source/target 两段 LLVM IR，构建它们的 SSA 抽象语义。
符号化执行（Symbolic Execution）
对于 source，记录输出 res1 = x + y；对于 target，记录 res2 = y + x。
生成等价性断言
构造一个 SMT-LIB 公式，断言“存在某组 x, y 使得 res1 ≠ res2”：

(set-logic QF_BV)                   ; 无量词位矢量
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
;; 如果能找到 x,y 使得 x+y ≠ y+x，则说明优化不合法
(assert (not (= (bvadd x y) (bvadd y x))))
(check-sat)

调用 SMT 求解器
Alive2 通常会调用 Z3、Boolector 或 CVC5，实际用的是其封装好的接口。
检查结果
如果 SMT 求解器返回 unsat，说明不存在反例；即对所有 x,y，都有 x+y = y+x，优化合法。如果返回 sat，它还会给出一组具体的 (x,y) 反例，表明在该输入下两段代码结果不一致，优化不合法。

数学领域的例子

下面我们用一个简单的 线性整数算术（Theory of Linear Integer Arithmetic, LIA）的例子，完整演示 DPLL (T) 框架如何解决 SMT 问题。

问题描述

令变量 $x,y\in\mathbb{Z}$ ，考虑以下公式 $F$ ：$$F = \bigl(x \ge 2 ;\wedge; y = x + 1\bigr) ;\wedge; \bigl(y < 2 ;\lor; x > 5\bigr).$$ 我们要判断：是否存在整数 $x,y$ 使得 $F$ 成立？并在可满足时给出一个模型。

1. 布尔抽象

先把每个“理论原子”替换成一个新的布尔变元 $P_i$ ：P1: $(x\ge2)$ , P2: $(y=x+1)$ , P3: $(y\lt2)$ , P4: $(x\gt5)$ . 那么 $$B(F) = P_1 \wedge P_2 \wedge (P_3 \lor P_4).$$ 这就是一个纯布尔公式。

2. SAT 层求解

我们用 CDCL SAT 求解器在 $B(F)$ 上搜索一个可行赋值。

可能的解： $\alpha_1:\{P_1=1,P_2=1,P_3=1,P_4=0\}$ （显然 $P_3\lor P_4$ 为真，其它也都选真。）SAT 引擎报告：可满足，并返回这个布尔模型 $\alpha_1$ 。

3. 构造理论子公式

把 $\alpha_1$ 映射回原始理论原子，得到一个纯 LIA 约束集：$$C = (x \ge 2)\wedge(y = x + 1)\wedge(y < 2).$$

4. 调用理论求解器（T-solver）

检查 $x\ge2,y=x+1,y<2$ 是否可满足？

从 $y=x+1$ 和 $y<2$ 得到 $x+1<2$ ，即 $x<1$ 。
又有 $x\ge2$ .
显然 $x<1$ 与 $x\ge2$ 冲突，UNSAT。
T-solver 会提取出导致矛盾的原子子集，映射回布尔层，生成一个冲突子句（theory lemma）：$$\ell_1 = \neg P_1 \lor \neg P_2 \lor \neg P_3.$$

5. 刷新布尔公式，重新 SAT

把 $\ell_1$ 加入到 $B(F)$ ：$$B(F):=P_1\wedge P_2\wedge(P_3\vee P_4);\wedge;(\neg P_1\vee\neg P_2\vee\neg P_3).$$ SAT 再次运行，找新的解。

一个可行的布尔模型是： $\alpha_2:\{P_1=1,P_2=1,P_3=0,P_4=1\}$ ，因为

$P_1,P_2$ 皆为真；
$P_3\lor P_4$ 由 $P_4=1$ 保证；
冲突子句 $\neg P_1\vee\neg P_2\vee\neg P_3$ 也成立（ $\neg P_3$ 为真）。

6. 再次理论检查

映射回 LIA： $x\ge2,y=x+1,x>5$ . 这组约束显然没有矛盾：例如取 $x=6,y=7$ 就满足 $6\ge2,7=6+1,6>5$ . T-solver 返回 SAT，并给出模型（比如 $(6,7)$ ）。

7. 结论

最终 SMT 过程返回 SAT，并给出一个具体整数模型 $x=6,y=7$ .
我们利用了 DPLL (T) 的惰性策略：
1. 先在布尔层剪枝 → 得到布尔候选
2. 再在理论层检查 → 若冲突生成 lemma 回传
3. 重复直到布尔层或理论层报出最终结果
  这样，SMT 求解器就高效地在“布尔搜索”和“理论决策”之间协同工作，既重用 SAT 引擎的强大能力，又利用专门的算术决策过程。