可满足性模理论 | Codeboy's Blog

形式陈述

固定签名 $\Sigma$ 与一个一阶理论 $T$ 。对通常为量词自由的 $\Sigma$ -公式 $\varphi$ ，SMT 问题判定是否存在 $\Sigma$ -结构 $\mathcal M$ 与变量赋值 $\nu$ ，使

\mathcal M\models T \qquad\text{且}\qquad \mathcal M,\nu\models\varphi.

若存在，返回的模型必须同时解释公式中的常元、函数和关系；若不存在，返回 UNSAT，理想情况下附带可检查的理论证明。常见理论包括等式与未解释函数 EUF、线性实数算术 LRA、线性整数算术、定宽位向量和数组。理论名称不是性能标签：它决定值域、运算、溢出和等式公理，因而决定公式本身的真假。

Boolean abstraction 把每个理论原子 $A_i$ 替换成命题变量 $p_i$ ，保留联结词结构。命题模型只是候选：对应的带符号理论文字集合还必须与 $T$ 一致。若 $T\models\neg(l_1\land\cdots\land l_k)$ ，理论求解器可返回子句

\neg l_1\lor\cdots\lor\neg l_k

排除这组 Boolean 选择。若公式含量词或落在不完备片段，求解器还可能返回 unknown；超时也不能解释为 UNSAT。

直觉

SAT 把原子看成可以独立取真的开关，SMT 则要求这些开关来自同一个数学世界。命题层可以选择“ $x\le y$ 为真”与“ $y<x$ 为真”，但实数序不允许二者同时成立。Theory solver 的工作就是检查候选开关是否能被具体数值、函数或数组实现，并把失败原因翻译回布尔层。

“模理论”也意味着所有推理相对于固定公理类。表达式 x+1>x 在线性整数或实数算术中有效，在定宽无符号位向量最大值处却失败；把程序整数默认为数学整数，得到的不是同一问题的近似答案，而是另一个理论中的答案。

例子与边界

在线性实数算术中考虑

\varphi=(x\le y)\land(y<x).

Boolean abstraction 为 $a\land b$ ，赋值 $a=b=1$ 是命题模型。理论层却把两个不等式合并成 $x\le y<x$ ，推出 $x<x$ ，因此无实数模型。相反，

(x\le y)\land(y\le x)

有模型 $x=y=0$ ，且理论还能推出 $x=y$ 。模型中的具体数值未必唯一；SMT SAT 只承诺存在一个解释，不承诺最小值或最优值。

CNF-SAT与 SMT 都使用 SAT/UNSAT 接口，却不能混用证书。纯 SAT 冲突由命题子句解释；SMT 冲突还需 theory lemma。一般一阶逻辑的可满足性不可判定，SMT 的成功来自选取可判定或可控片段，并不表示任意量词、非线性整数算术和递归定义都已有完整算法。浮点、数组外延性与未解释函数也各有不同模型边界。

推论与应用

DPLL(T) 框架实现常见的 lazy SMT：SAT 引擎提出 Boolean trail，专用 theory solver 增量检查并提供冲突或传播解释。Eager 路线则可把位向量 bit-blast 成纯 CNF；两者只在编码与理论语义完整对齐时给出同一答案，不能因都调用 SAT 就视为同一算法。

程序验证、符号执行、调度和合成使用 SMT 表达值域约束。工具返回的模型仍需映射回源对象，并核对前端是否编码了溢出、别名、未定义行为和环境假设。保存 SMT-LIB 输入、逻辑名称、求解器版本与 proof/model 输出，才能区分求解错误、建模错误和不可复现的资源失败。

参考资料

Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli, “Satisfiability Modulo Theories,” in Handbook of Satisfiability, 2nd ed., IOS Press, 2021。
Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View, 2nd ed., Springer, 2016, Chapters 4–12。
Clark Barrett, Pascal Fontaine, and Cesare Tinelli, The Satisfiability Modulo Theories Library (SMT-LIB): Version 2.6, 2017。

形式陈述 ​

反向链接

形式陈述