DPLL(T) 框架

Boolean 层善于处理大量析取选择，理论层善于处理一组合取原子之间的数学约束。DPLL(T) 不让任一方独自承担全部公式：SAT 引擎先提出候选组合，理论求解器发现其中不可实现的局部核心，再把这个核心翻译成 SAT 能记住的子句。后续所有 Boolean 搜索都会避开同一理论矛盾。

这种惰性分工避免预先枚举理论的全部公理实例。Theory solver 可以增量保留等价类、tableau 或数组约束，随 trail push/pop 更新；布尔引擎则把理论解释当作普通 reason。接口越小，越容易证明协作可靠，但模型构造、组合理论与证书仍不能被省略。

在线性实数算术中取

令 $a,b,c$ 分别代表 $x\le 0,x\ge 2,x=1$，Boolean abstraction 为 $(a\vee b)\wedge c$。根层先传播 $c$；若 SAT 引擎选择 $a$，theory solver 检查 $x\le 0,x=1$ 后返回解释 $\{a,c\}$，学习 $\mathrm{\neg }a\vee \mathrm{\neg }c$。在 $c$ 为真时它传播 $\mathrm{\neg }a$，原子句遂传播 $b$。集合 $\{b,c\}$ 又要求 $x\ge 2$ 且 $x=1$，理论返回 $\mathrm{\neg }b\vee \mathrm{\neg }c$。现在 $a,b$ 均假，与 $a\vee b$ 根层冲突，故公式 UNSAT。

每条 theory lemma 都可独立核验；若第一次解释错误地只含 $a$，学习 $\mathrm{\neg }a$ 就声称 $T\models x>0$，会排除合法模型。另一个边界是 partial checking：某些 solver 只在 Boolean total assignment 后检查理论一致性，仍可完整但会探索更多伪模型；提前 check 与 propagation 是效率增强，不应冒充可靠性来源。

量词、非凸理论和多理论组合会扩大接口责任。一个 solver 对自身文字集返回“consistent”，不必然保证几个 solver 的局部模型能合成共同模型；组合过程还要交换共享等式或安排。超时与不完整实例化应返回 unknown，不能伪装成 SAT 或 UNSAT。

DPLL(T) 允许复用成熟 CDCL 的 watched literals、学习和 assumptions，同时为 EUF、LRA、数组等理论插入专用状态。Theory lemma 一旦加入布尔数据库可跨 restart 复用；若它依赖临时 assumption，必须让条件文字留在子句中，以免下一次增量查询错误继承无条件结论。

Proof-producing SMT 会把 Boolean resolution 与理论证明拼接。检查器需要验证每个 theory lemma 的理论有效性，再验证布尔归结最终导出空子句。模型端则需把 Boolean 原子值、理论赋值和未解释函数解释合成一个结构；只打印部分数值而不验证所有原子，不能算完整 SAT 证书。