> For AI agents: the complete documentation index is available at https://shijin.space/llms.txt, the full documentation bundle is available at https://shijin.space/llms-full.txt.

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

前置知识：[SAT 与 DPLL](https://shijin.space/knowledge/sat-dpll/index.md)中的部分赋值、归结与变量消除，以及 [CDCL](https://shijin.space/knowledge/sat-cdcl/index.md) 中的传播、学习和回跳。

## 变换的目标与适用范围

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

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

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

对判定问题，等可满足足以保留答案；若应用还需要原变量上的解，就必须维护恢复信息。对于 UNSAT，也应把公式变换纳入可检查的证明，而不能只证明简化后的公式无解 \[[1, sec. 9.5](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

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

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

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

把子句看成文字集合。若 $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](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

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

考虑

$$
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](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

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

### 失败文字试探

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

例如

$$
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](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

例如

$$
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](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

候选变量未通过预算时，可以保留原公式，不必强行消去全部变量。预处理中的 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](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

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

恢复 $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 检查集合中的每个文字是否为假，空集合的检查结果为真。

```pseudocode
\begin{algorithm}
\caption{Model Reconstruction after Variable Elimination}
\begin{algorithmic}
\FUNCTION{RestoreModel}{$\alpha,S$}
    \WHILE{$S\ne\varnothing$}
        \STATE $(x,P,N)\gets$ \CALL{Pop}{$S$}
        \STATE $\alpha[x]\gets 0$
        \FORALL{$C\in P$}
            \IF{\CALL{AllFalse}{$C\setminus\{x\},\alpha$}}
                \STATE $\alpha[x]\gets 1$
            \ENDIF
        \ENDFOR
    \ENDWHILE
    \RETURN $\alpha$
\ENDFUNCTION
\end{algorithmic}
\end{algorithm}
```

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

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

内处理把公式变换插入搜索阶段之间。它可以处理当前公式中的原始子句和学习子句，并不局限于后者。例如，学习或传播暴露了新的短子句后，可能触发新的子句吸收、强化或变量消除 \[[1, sec. 9.1](https://shijin.space/knowledge/sat-preprocessing/index.md#ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing)\]。

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

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

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

## 参考文献 {#references-sat-preprocessing}

<div id="refs-sat-preprocessing" class="references csl-bib-body">

<div id="ref-sat-preprocessing-BiereJarvisaloKiesl2021Preprocessing" class="csl-entry">

1\. Armin Biere, Matti Järvisalo, and Benjamin Kiesl. *Preprocessing in SAT solving*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200992).

</div>

</div>

## 配套演示

- [现代 SAT 求解器：传播、搜索策略与内处理 · 16:9](https://shijin.space/slides/sat-implementation/index.html)
- [现代 SAT 求解器：传播、搜索策略与内处理 · 4:3](https://shijin.space/slides/sat-implementation/index-4-3.html)