SMT 理论传播

Boolean unit propagation 只能读取已有子句，theory propagation 则让背景数学主动生成一条当前有用的子句。例如两个不等式的传递性不是 CNF 的语法规则，但理论求解器可以把它压成一个三文字 lemma；从此 SAT 引擎无需理解实数序，也能复用这项结论。

这是一座带证明回执的桥。Theory solver 不能只说“我算出 $\ell$”，而要指出 trail 中哪些文字足以推出它。回执让冲突分析穿过理论传播节点，最终学习的混合子句仍有可验证来源。

在线性实数算术中，令

当 trail 含 $a,b$ 且 $c$ 已在 Boolean 原子表中，传递性给出

因此返回 explanation $\mathrm{\neg }a\vee \mathrm{\neg }b\vee c$，并传播 $c$。若 trail 还含 $d:(z<x)$，则 $a,b,d$ 共同推出 $x<x$，可返回 conflict clause

逐项代入即可检查：前三个原子不可能在同一实数赋值下为真。

边界之一是未登记后果。如果公式从未提及 $x\le z$，solver 可以只做一致性检查而不新建 $c$；这不损害完整性，只可能错过剪枝。另一个边界是浮点近似：用数值容差“似乎推出”某原子不能直接产生可靠 theory lemma，除非有区间证书或精确重检。对于非凸理论，局部信息可能只推出 $a=b\vee a=c$，无法任选一个等式传播；必须让 Boolean 层分裂析取。

在 EUF 中，同余闭包算法公理库同余闭包算法Congruence closure algorithm · EUF congruence closure计算地面项等式生成的最小函数同余，并以此判定 EUF 等式与不等式合取是否一致。可对已登记等式原子传播“参数相等蕴含函数值相等”，并为 disequality 冲突重建等式链。在 LRA 中，SMT 单纯形求解器公理库线性实数算术 SMT 的单纯形算法LRA SMT simplex algorithm · Simplex for linear real arithmetic · SMT simplex维护线性 tableau 与变量界以增量判定 LRA 文字合取可行性，并生成理论冲突解释。可从 tableau 行和活动边界解释界传播或不可行冲突。二者只在各自理论和解释接口下实现 theory propagation，不是可互换的通用算法。

Early propagation 往往减少 Boolean 决策，却也消耗 theory solver 时间；exhaustive theory propagation 不必在所有实例上更快。增量求解器还要让 explanation 的前提随 push/pop 正确存活。证明日志可把每条 theory lemma 交给专门 checker，随后继续使用普通 SAT checker 验证全局归结。