SAT 预处理、内处理与模型恢复#

前置知识：SAT 与 DPLL中的部分赋值、归结与变量消除，以及 CDCL 中的传播、学习和回跳。

#变换的目标与适用范围

预处理（preprocessing）在主要搜索开始前变换公式；内处理（inprocessing）把这类变换与搜索交替执行。两者都希望降低整个求解过程的成本，例如删除重复约束、加强传播或减少活动变量。公式较小不自动意味着求解较快：删去的冗余子句也可能原本有助于传播，因此需要考虑变换开销与后续搜索效果 [1, sec. 9.1]。

本文先讨论一次 CNF 可满足性查询，不包含之后追加约束或临时假设的增量调用。令 $F$ 为变换前的公式、$G$ 为变换后的公式，需要分别回答：

• 是否保留所有模型，即在相同变量含义下有 $F\equiv G$？
• 是否只保留“有解或无解”的答案，即 $F$ 与 $G$ 等可满足？
• 若变量或模型集合发生变化，怎样把 $G$ 的模型恢复成 $F$ 的模型？

对判定问题，等可满足足以保留答案；若应用还需要原变量上的解，就必须维护恢复信息。对于 UNSAT，也应把公式变换纳入可检查的证明，而不能只证明简化后的公式无解 [1, sec. 9.5]。

#删除子句与删除文字是相反方向的操作

删除整个子句会减少约束，可能增加模型；从子句中删除文字会减少满足该子句的选择，可能减少模型。因此，“删除冗余内容”必须说明删的是子句还是文字，以及冗余依据是什么。

#子句吸收：删除已被更强子句蕴含的约束

把子句看成文字集合。若 $C\subseteq D$，则 $C$ 蕴含 $D$，称 $C$ 吸收 $D$（subsumption）。只要 $C$ 保留在公式中，就可以删除 $D$ 而不改变模型集合。例如

$$(a\lor b)\land(a\lor b\lor c)\equiv(a\lor b).$$

被删除的是较长、较弱的子句，不能反过来删除唯一的较强约束 [1, sec. 9.2.4]。

#自包含归结：有依据地强化一个子句

考虑

$$C=(x\lor a),\qquad D=(\neg x\lor a\lor b).$$

对 $x$ 归结得到 $R=(a\lor b)$，它的文字集合包含于 $D$。因此可以保留 $C$，用 $R$ 替换 $D$：

$$C\land D\equiv C\land R.$$

正向等价来自归结的可靠性；反向等价来自 $R\models D$。这称为自包含归结（self-subsuming resolution），净效果是删除 $D$ 中的 $\neg x$。它与学习子句的局部最小化使用相同的推理依据，但这里直接用于公式中的子句 [1, sec. 9.2.4.3]。

#试探传播与纯文字：必需的赋值和可选的赋值

#失败文字试探

临时假设文字 $\ell$ 为真，执行单位传播。如果得到冲突，就证明 $F\land(\ell)$ 不可满足，因此 $F\models\neg\ell$；可以把单位子句 $(\neg\ell)$ 加入公式，并撤销试探过程中临时产生的其他赋值。这称为失败文字试探（failed-literal probing） [1, sec. 9.2.2]。

例如

$$F=(\neg x\lor y)\land(\neg x\lor\neg y).$$

原公式没有单位子句。假设 $x=1$ 后，两个子句分别要求 $y=1$ 与 $y=0$，所以可以推出 $x=0$。加入 $(\neg x)$ 保持逻辑等价，因为它是原公式的必然结论。一次试探没有产生冲突，则不能据此宣布该文字可扩展为模型；单位传播本身并不完备。

#纯文字消除

若文字 $p$ 出现在公式中，而 $\neg p$ 不出现，就称 $p$ 为纯文字。把 $p$ 置真可以满足所有含它的子句，又不会使其他子句变假，因此可以删除这些子句，并记录恢复时令 $p$ 为真。这样的操作保持可满足性，但不必保持全部原始模型 [1, sec. 9.2.3]。

例如

$$F=(p\lor a)\land(\neg a\lor b),\qquad G=(\neg a\lor b).$$

$G$ 的任意模型都能通过令 $p=1$ 扩展成 $F$ 的模型。但 $F$ 也有 $p=0,a=b=1$ 的模型，所以 $F$ 并不蕴含 $p$。若直接加入单位子句 $(p)$，就会失去这部分合法模型，虽然 SAT/UNSAT 答案没有改变。

因此，纯文字的取值不能被解释成原公式必然推出的事实。固定值属于哪一种语义，需要与公式变换和恢复记录一起说明；前面基本 CDCL 中“根层赋值由原公式推出”的前提不能无条件沿用到所有预处理选择。

#有界变量消除：限制归结产生的规模

对变量 $x$，把公式拆成正出现子句、负出现子句和其余部分：

$$F=H\land\bigwedge_{i=1}^{m}(x\lor A_i) \land\bigwedge_{j=1}^{n}(\neg x\lor B_j),$$

其中 $H,A_i,B_j$ 都不含 $x$。加入全部非重言的归结式 $A_i\lor B_j$，再删除含 $x$ 的原子句，得到

$$G=H\land\bigwedge_{i,j}(A_i\lor B_j),\qquad G\equiv\exists x\;F.$$

这正是 DP 变量消除。为了避免反复消元导致公式膨胀，有界变量消除（bounded variable elimination，BVE）仅在代价符合预算时执行。例如，一种简单规则是：去重后的新增非重言子句数不超过被删除的子句数。实际实现还可以限制候选出现次数、归结式长度和检查工作量，也可能允许有限的规模增长；这些是代价控制规则，不改变消元的逻辑依据 [1, sec. 9.3.1]。

候选变量未通过预算时，可以保留原公式，不必强行消去全部变量。预处理中的 BVE 以改善后续搜索为目的，也不要求单靠消元完成 SAT 判定。

#从简化公式的模型恢复原变量

#连续消去两个变量的例子

考虑

$$F=(x\lor a)\land(\neg x\lor b)\land(\neg a\lor b).$$

先消去 $x$，把前两个子句归结为 $(a\lor b)$，保留第三个子句，得到

$$G=(a\lor b)\land(\neg a\lor b).$$

再消去 $a$，得到单位子句公式

$$H=(b).$$

两次消元分别把三个子句减为两个、两个减为一个，均符合不增加子句数的预算。求解 $H$ 得到 $b=1$，但这还不是原公式全部变量上的模型。

消去变量时，把变量和当时被删除的子句压入恢复栈。恢复时按相反顺序处理：

1. 先恢复 $a$。在 $b=1$ 下，$(a\lor b)$ 和 $(\neg a\lor b)$ 已经满足，可以选择 $a=0$。
2. 再恢复 $x$。此时原子句 $(x\lor a)$ 变成对 $x$ 的单位要求，所以取 $x=1$；另一个原子句 $(\neg x\lor b)$ 已被 $b=1$ 满足。

得到原公式的模型

$$(x,a,b)=(1,0,1).$$

逆序恢复有具体原因：消去 $x$ 时保存的约束可能依赖之后才被消去的 $a$；先恢复 $a$，才能据此选择 $x$。变量消除保存的是存在量化后的条件，不能把所有被消去变量任意补成同一个值 [1, sec. 9.5.1]。

#为什么总能选择一个可行的取值

恢复 $x$ 时，其余相关变量已经取值，并满足消去 $x$ 后留下的归结式。若某个正出现子句 $x\lor A_i$ 的 $A_i$ 全为假，就必须取 $x=1$。此时不可能又有某个负出现子句 $\neg x\lor B_j$ 的 $B_j$ 全为假，否则归结式 $A_i\lor B_j$ 也会为假，与已有模型矛盾。若没有正出现子句要求 $x=1$，取 $x=0$ 就能满足全部负出现子句，同时正出现子句已由其他文字满足。

下面用伪代码表示这种恢复方式。栈中每项记录被消去变量 $x$，以及当时正、负出现的子句集合 $P,N$；输入 $\alpha$ 给所有未被消去的变量赋值，并满足最终简化公式，已不出现在简化公式中的自由变量可以任意补全。AllFalse 检查集合中的每个文字是否为假，空集合的检查结果为真。

负出现子句不必再独立决定 $x$：上述归结式的满足性已经排除了正、负子句同时提出相反要求的情况。这里选择了一种容易说明的恢复规则；栈和赋值查询的实现未展开，伪代码不能独立运行，也不直接涵盖任意其他公式变换。若还进行了单位传播、等价文字替换等操作，也要保存相应固定值或映射，并按它们的依赖关系恢复。

#将预处理方法放回 CDCL 搜索中

内处理把公式变换插入搜索阶段之间。它可以处理当前公式中的原始子句和学习子句，并不局限于后者。例如，学习或传播暴露了新的短子句后，可能触发新的子句吸收、强化或变量消除 [1, sec. 9.1]。

一种便于理解的安排是回到根层，再执行一轮有预算的变换；这不是所有内处理方法必须采用的唯一安排。继续搜索前，需要完成新单位子句的传播，并让活动变量、监视列表、阻塞文字缓存和原因引用对应当前公式。删除仍被用作传播原因的子句时，不能留下悬空的原因记录。

此外，还要保留两类结果之间的连接：SAT 时将模型恢复到原问题的变量；UNSAT 时为公式变换留下相应证明信息。若应用之后还要对被消去变量追加约束或传入假设，仅保持这一次查询等可满足并不足够，需要增量接口另外保护或恢复相关变量 [1, secs. 9.1, 9.5]。这两项责任分别在结果验证与增量 SAT中展开。

评价一种变换时，应把变换时间、后续搜索时间以及需要的恢复和验证成本合起来考虑。减少变量数、子句数或文字数可以描述变换效果，但不能单独作为求解性能改善的证据。

#参考文献