SAT 求解结果的验证：模型、UNSAT 证明与检查器#

前置知识：SAT 与 DPLL中的模型、单位传播和归结，以及预处理与内处理中的等可满足变换与模型恢复。

#验证对象是求解结果及其证据

求解器可能使用复杂的数据结构、启发式和公式变换。即使算法原理正确，具体实现也可能出错。结果验证把“寻找答案”和“检查证据”分开：求解器产生模型或证明，检查器依据输入公式和明确的规则判断这些证据是否成立 [1, sec. 15.1]。

SAT 和 UNSAT 的证据不同。SAT 给出一个使全部约束成立的赋值；UNSAT 要说明不存在任何这样的赋值。资源耗尽而返回 UNKNOWN 不属于其中任何一种结论，也没有因此得到原问题的反证。

#SAT：把模型代回原始公式

设输入 CNF 为 $F=C_1\land\cdots\land C_m$，给定对全部输入变量的赋值 $\alpha$，只需检查每个子句是否至少有一个真文字：

若赋值查询为常数时间，检查所需工作量至多与输入中的文字出现总数成线性关系。这里线性的是给定模型后的检查，不是寻找模型 [2, sec. 4.4.1.4]。

例如

$\alpha=(a,b,c)=(1,0,1)$ 使三个子句分别由 $a,c,\neg b$ 满足。若把 $c$ 改成 $0$，第二个子句立即失败，因此不能把这个错误赋值作为 SAT 证据。

若求解器先消去了变量，返回简化公式的模型还不够。必须按恢复记录得到原变量上的赋值，再检查原始输入。编码中引入的辅助变量与业务变量也要区分：先验证编码后的公式，再把业务变量投影回原问题；模型投影的依据见 SAT 与 DPLL中的 Tseitin 编码。

#UNSAT：逐步加入可以检查的结论

一个常用思路是记录子句序列

检查器从输入公式开始，逐步验证每次加入是否符合规定，最后接受空子句。空子句对任何赋值都为假，因此一条有效推导能够证明输入无解。中间步骤需要可执行的检查规则，不能只写“这个子句显然冗余” [1, sec. 15.2]。

#RUP：否定待检查子句，再做单位传播

令待检查子句为 $C=(\ell_1\lor\cdots\lor\ell_r)$。要使它为假，必须让其中每个文字都为假。把这些取值作为临时单位假设，若单位传播得到冲突，就说明当前公式 $F$ 蕴含 $C$：

这个检查称为逆向单位传播（reverse unit propagation，RUP）。它利用普通的正向传播检查一个候选结论，不需要重复求解器原来的分支搜索。检查失败只表示没有通过这项规则，不能断言 $F$ 不蕴含 $C$；单位传播并不完备 [1, sec. 15.2.2]。

#四个子句组成的完整反证

考虑

原公式没有单位子句，直接单位传播不会前进。可以提交以下三个添加步骤：

1. 加入 $D_5=(a)$。临时假设 $\neg a$，由 $D_1$ 得到 $b$，再与 $D_2$ 冲突，因此 $D_5$ 通过 RUP 检查。
2. 加入 $D_6=(\neg a)$。临时假设 $a$，由 $D_3$ 得到 $b$，再与 $D_4$ 冲突，因此 $D_6$ 也通过检查。
3. 加入 $D_7=\varnothing$。空子句没有需要额外否定的文字；当前数据库已有 $(a)$ 和 $(\neg a)$，直接传播即得到冲突。

每一步都从独立的临时赋值开始，但前面已经验证的子句继续保留在数据库中。这份证明不是最短写法：加入 $(a)$ 后，原公式的另两个子句已经足以继续传播到冲突；这里保留两个对称步骤，便于观察 RUP 如何检查正、负两个方向。

下面是只接受 RUP 添加步骤的教学检查器。PropagateConflict 从空赋值开始，用 $A$ 中的单位假设和 $F$ 中的单位子句传播，遇到矛盾返回真；它不调用完整 SAT 搜索。

这里的 $\pi$ 是有序序列，FOR ALL 按记录顺序遍历；每次传播结束都丢弃临时假设。输入解析和传播实现未展开，伪代码不能独立运行，也不支持子句删除或 RAT 步骤。读到有效空子句即接受；只有若干有效中间子句而没有空子句，仍不是完整的 UNSAT 证明。

#DRAT：允许更广的添加规则与子句删除

RUP 足以表达许多基本 CDCL 学习步骤，但某些重编码与公式变换需要更强的冗余规则。DRAT 允许符合 RAT 条件的子句添加，以及子句删除；检查器在每一步都针对当时的数据库解释规则 [1, secs. 15.2.4.1, 15.2.5]。

RAT 的思路是选定子句中的一个主元文字，检查它与数据库中含相反文字的子句之间的局部关系。本文不展开完整判定过程，但必须区分它与逻辑蕴含：合法 RAT 添加可以只保持可满足性，而不保留全部原模型。

例如 $F=(p\lor q)$ 中没有 $\neg p$。添加 $(p)$ 时，以 $p$ 为主元，没有含相反文字的子句需要检查，因而满足 RAT 条件。添加前后都可满足，但原模型 $p=0,q=1$ 被排除了，说明 $F$ 并不蕴含 $p$。这与纯文字消除涉及的语义差别相通。

子句删除还需要另一层区分。删除约束可能把 UNSAT 公式变成 SAT，因此它一般不保持等可满足；但在反证检查中，删除保留了“如果原来有模型，删除后仍有模型”的方向。合法添加也不能把一个可满足状态变成不可满足状态。沿整条记录，如果最终合法地得到空子句，就能反推出初始公式不可能有模型。这说明为什么 UNSAT 证明中的删除步骤无需另外证明被删子句受到其余子句蕴含；这不等于求解器可以任意删掉原始约束后把一个 SAT 赋值直接交给用户 [1, sec. 15.2.5]。

#LRAT：给检查器提供明确的子句提示

只有新子句时，检查器还要寻找哪些已有子句能够完成传播。LRAT 为子句分配标识，并提供用于检查的提示，使检查器少做搜索。格式既支持 RUP 步骤，也支持更一般的 RAT 步骤；提示本身必须核对，不能因为写出了编号就直接信任。原始工作给出了 Coq 和 ACL2 中经过形式化验证的检查器 [3, secs. 3–6]。

将上面的 $a,b$ 分别编号为 $1,2$，输入文件可以写成 DIMACS：

p cnf 2 4
1 2 0
1 -2 0
-1 2 0
-1 -2 0

前四个输入子句依次具有标识 $1,2,3,4$。对应的一份 LRAT 记录为

5 1 0 1 2 0
6 -1 0 3 4 0
7 0 5 6 0

第一行的含义是：新子句标识为 $5$，内容是文字 $1$，第一个 $0$ 结束子句，后面的 $1,2$ 是按顺序使用的输入子句标识，最后一个 $0$ 结束提示。检查时先假设 $a=0$，子句 $1$ 传播 $b$，子句 $2$ 随即冲突。最后一行内容为空，依次使用子句 $5,6$ 即产生矛盾。这里全是 RUP 步骤，也属于 LRAT 的 RUP 子集。

与之对应，不带提示的添加记录可以只写为 1 0、-1 0、0。更少的记录信息不一定意味着总成本更低，因为检查器可能需要花更多时间寻找推理依据；应同时考虑生成时间、文件体积和验证时间 [1, secs. 15.4, 15.6]。

#公式变换也必须进入验证链条

设预处理把原公式 $F$ 变成 $G$。验证 $G$ 的 UNSAT 证明，只能直接证明 $G$ 无解；还需要可检查的变换记录，把这个结论连接回 $F$。SAT 情况对应模型恢复，UNSAT 情况对应变换的证明责任，两者不能互相替代 [1, sec. 15.5]。

增量调用还多出查询上下文。同一个永久公式在不同假设下可能分别得到 SAT 和 UNSAT，因此证明需要明确对应哪一次查询、哪些假设和哪些追加约束。上一节的 RAT 例子也提示：只对当前公式保持可满足性的操作，未必在以后任意追加约束时仍然安全。

CaDiCaL 3.0 将带提示的证明生成扩展到更多内处理，并讨论了含扩展变量的增量证明格式 LIDRUPE。这一进展说明，验证支持需要与公式变换及调用接口共同设计；不能只把一个求解器的“支持证明”理解为它所有运行模式都自动具有同样的证据 [4, secs. 2, 4]。

#检查通过之后，结论覆盖到哪里

独立检查器降低了对复杂求解器实现的依赖，但仍需要明确它检查的是哪一个输入、哪一种证明格式，以及实现的可信依据。运行过测试的检查器与经过形式化验证的检查器具有不同的证据强度；形式化验证也要核对其涵盖的解析、逻辑核心及执行环境。

更外层还有建模责任。若“每班必须有人”被误编码成“每人必须上班”，一个完全正确的求解器与检查器仍然只会处理错误的公式。因此完整流程需要把应用约束、编码公式、求解证据和业务结果的解释连接起来。下一篇增量 SAT 与建模实践用一个小型排班问题展示这条连接。

#参考文献