> 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)中的 CNF 编码，以及[结果验证](https://shijin.space/knowledge/sat-result-verification/index.md)中的模型检查和查询证据。

## 从一次判定变成一系列相关查询

许多应用反复求解相似问题：基础约束保持不变，只增加部分约束，或在不同调用中尝试不同条件。每次重新构造一个求解器会丢掉能够复用的信息。增量 SAT 让求解器跨调用维护公式和合法的学习信息；具体性能收益仍取决于查询序列与实现 \[[1, sec. 4.4.1.2](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-MarquesSilvaLynceMalik2021CDCL)\]。

用 $F_t$ 表示第 $t$ 次调用时的永久公式，用 $A_t$ 表示这次调用的假设文字集合。实际查询是

$$
F_t\land\bigwedge_{\ell\in A_t}(\ell).
$$

追加永久子句得到 $F_{t+1}=F_t\land\Delta_t$；更换假设则只改变当前查询。在标准的假设接口中，本次假设用完即清除，需要下次继续使用的假设必须重新提交。把临时要求误当成永久单位子句加入，会改变以后所有查询的含义 \[[2](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-SATCompetition2020IPASIR)\]。

## 一个两人两班的编码

设人员为甲、乙，班次为 $1,2$。布尔变量 $a_i$ 表示甲承担第 $i$ 班，$b_i$ 表示乙承担第 $i$ 班。背景约束是每班恰好一人：

$$
B=\bigwedge_{i=1}^{2}
\bigl((a_i\lor b_i)\land(\neg a_i\lor\neg b_i)\bigr).
$$

其中第一个子句保证至少一人，第二个保证不能两人同时承担。因为这里只有两名候选人，恰好一人的 CNF 很简单；候选人数增加时，至多一人的编码选择还会影响规模和传播效果。

接下来希望按需开启四组要求：

1. $G_1=\{(\neg a_1\lor\neg a_2)\}$：甲至多承担一班。
2. $G_2=\{(\neg b_1\lor\neg b_2)\}$：乙至多承担一班。
3. $G_3=\{(\neg a_1)\}$：甲不能承担第 $1$ 班。
4. $G_4=\{(\neg a_2)\}$：甲不能承担第 $2$ 班。

这些要求可能互相冲突，但并非每次查询都需要全部开启。将它们与背景约束分开，也让后续的冲突解释能够回到具体业务要求。

## 激活文字：用假设控制一组子句

为每组 $G_i$ 引入一个新的选择变量 $s_i$。把组内每个子句 $C$ 改成带保护条件的子句 $\neg s_i\lor C$，永久加入

$$
F=B\land\bigwedge_{i=1}^{4}\ \bigwedge_{C\in G_i}(\neg s_i\lor C).
$$

这里固定约定：假设 $s_i=1$ 时，保护文字 $\neg s_i$ 为假，必须满足 $C$，所以该组开启；假设 $s_i=0$ 时，保护文字为真，整组子句自动满足，所以该组关闭。一组可以包含多个子句，只要共用同一个选择变量即可 \[[1, sec. 4.4.1.2](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-MarquesSilvaLynceMalik2021CDCL)\]。

如果选择变量只以这些负保护文字出现，省略 $s_i$ 的假设也允许求解器把它取为假，因此不会强制开启该组。为了明确展示开关状态，本例在普通查询中显式给出正、负两种假设。选择变量不应再被误用为业务变量或参与无关约束，否则这种关闭解释需要重新检查。

### 第一次查询：得到一个合法排班

开启 $G_1,G_2,G_3$，关闭 $G_4$，即使用

$$
A_1=\{s_1,s_2,s_3,\neg s_4\}.
$$

$G_3$ 要求 $a_1=0$，背景约束推出 $b_1=1$；$G_2$ 再推出 $b_2=0$，背景约束推出 $a_2=1$。得到

$$
(a_1,b_1,a_2,b_2)=(0,1,1,0).
$$

业务含义是乙承担第 $1$ 班、甲承担第 $2$ 班。这个赋值满足背景约束和三个已开启的要求；关闭的 $G_4$ 不参与本次业务要求。完整 SAT 模型还应包含与假设一致的选择变量取值。

### 第二次查询：相同永久公式，不同结论

开启全部要求，改用

$$
A_2=\{s_1,s_2,s_3,s_4\}.
$$

$G_3,G_4$ 要求 $a_1=a_2=0$，于是背景约束要求 $b_1=b_2=1$，与 $G_2$ 冲突。此时查询结果是 UNSAT，但永久公式 $F$ 仍然可满足，例如把所有选择变量关闭后，只需满足每班恰好一人。

因此这次结论必须读成“$F$ 在 $A_2$ 这组假设下无解”，不能省略假设上下文。撤掉 $s_4$ 并重新提交第一次的假设，仍能得到第一次的可行排班。

## 不可满足核心：解释哪些假设已经足以冲突

假设核心是一个子集 $K\subseteq A$，满足

$$
F\land\bigwedge_{\ell\in K}(\ell)\ \text{is UNSAT}.
$$

等价地，永久公式蕴含禁止这些假设同时成立的子句：

$$
F\models\bigvee_{\ell\in K}\neg\ell.
$$

在上面的第二次查询中，$K=\{s_2,s_3,s_4\}$ 已足够。它对应“乙最多一班，但甲两班都不能上”；$G_1$ 与这次矛盾无关。由激活文字得到的是相对于背景 $B$ 的约束组核心，不是在保证每组内部的所有子句都不可再删 \[[1, sec. 4.4.1.3](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-MarquesSilvaLynceMalik2021CDCL)\]。

通常应区分三种要求：一个**不可满足核心**只需足以冲突；**子集极小核心**还要求删去其中任何一项后都可满足；**最小核心**则要求在所有核心中元素数最少。求解器返回的核心通常只满足第一项，不能直接把它称为最小解释。

本例中的三项核心恰好是子集极小的：去掉 $s_2$，允许乙承担两班；去掉 $s_3$，可由甲承担第 $1$ 班、乙承担第 $2$ 班；去掉 $s_4$，可交换两人的班次。每次都能给出满足剩余要求的模型，因此每项在这个核心中都不可删除。

### 用额外查询缩减核心

给定一个已经确认不可满足的假设核心 $K$，可以逐项试删。如果移除某项后仍为 UNSAT，就保留这次删除；如果变为 SAT，就把该项留下。以下伪代码假设整个过程中永久公式 $F$ 不变。

```pseudocode
\begin{algorithm}
\caption{Deletion-Based Assumption Core Reduction}
\begin{algorithmic}
\FUNCTION{ReduceCore}{$F,K$}
    \STATE $U\gets K$
    \FORALL{$\ell\in\operatorname{Snapshot}(U)$}
        \STATE $r\gets$ \CALL{SolveUnder}{$F,U\setminus\{\ell\}$}
        \IF{$r=\mathrm{UNSAT}$}
            \STATE $U\gets U\setminus\{\ell\}$
        \ELIF{$r=\mathrm{UNKNOWN}$}
            \RETURN $(U,\mathrm{false})$
        \ENDIF
    \ENDFOR
    \RETURN $(U,\mathrm{true})$
\ENDFUNCTION
\end{algorithmic}
\end{algorithm}
```

SolveUnder 每次使用恰好给定的临时假设调用同一个增量求解器，不把它们作为永久子句加入，也不继承上次的临时假设。Snapshot 固定初始遍历顺序。返回值中的布尔量表示是否已完成子集极小性的检查；遇到 UNKNOWN 时，$U$ 仍是已知不可满足的核心，但不能确认它极小。辅助接口未展开，这是一份算法伪代码，不能独立运行。

为什么一次遍历足够？某项被保留时，去掉它的查询已经得到 SAT；之后只可能移除更多假设，使约束更弱，之前的满足赋值仍是该项不可再删的见证。因此所有查询都给出确定结果时，最后得到子集极小核心。试删顺序可能产生不同核心，也不保证元素数全局最少；最多进行 $|K|$ 次额外调用，不表示这些调用总能很快完成。

若从本例的四项集合开始，按 $s_1,s_2,s_3,s_4$ 的顺序试删，先删除与冲突无关的 $s_1$，随后三次删除都得到 SAT，最终留下 $\{s_2,s_3,s_4\}$。

## 调用接口时保留正确的状态与语义

IPASIR 把这些操作组织成一个较小的接口。`ipasir_add` 逐文字构造永久子句，以 `0` 结束；`ipasir_assume` 添加下一次查询的假设；`ipasir_solve` 返回 `10`、`20` 或 `0`，分别表示 SAT、UNSAT 或中止而未取得结论。调用结束后假设清空，永久子句仍保留 \[[2](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-SATCompetition2020IPASIR)\]。

只在返回 SAT 后读取 `ipasir_val`，只在返回 UNSAT 后对本次假设读取 `ipasir_failed`。这些结果应在下一次添加子句或假设前取出，因为状态变化后旧结果不再是接口保证可读的当前结果。`ipasir_val` 返回 `0` 不能直接解释成文字为假；应按求解器的模型约定处理未指定取值，并完成模型检查。

在基本 CDCL 的假设求解中，临时假设作为带边界的决策参与搜索；学习子句必须保留必要的假设依赖，而不能把假设本身误认为永久事实。只有对持续有效的数据库仍然合法的学习信息才能跨调用复用。上面的核心子句 $\neg s_2\lor\neg s_3\lor\neg s_4$ 就可以保留：它禁止三组要求同时开启，但不阻止关闭其中一组后的新查询。

## 增量调用怎样与预处理配合

单次查询中合法的等可满足变换，不一定能直接承受未来对任意原变量追加约束。例如原公式 $(x\lor y)$ 可通过令纯文字 $x=1$ 简化；但以后若追加 $(\neg x)$，原问题仍有 $x=0,y=1$ 的模型，不能继续把之前选择的 $x=1$ 当成永久蕴含事实。

因此增量预处理需要维护外部变量与内部表示之间的关系。可行机制包括保护可能再次使用的变量、限制某些变换，或在后续调用需要时恢复被删除的子句。CaDiCaL 的实现使用按需恢复机制，使预处理与内处理能够用于增量场景；这不同于要求调用者手工禁止全部化简 \[[3, secs. 1–2](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-BiereEtAl2024Cadical)\]。

证明也需要对应具体查询。若希望独立核验假设核心 $K$，需要检查 $F\land\bigwedge_{\ell\in K}(\ell)$ 的 UNSAT 证据；只看到几个 `failed` 标记，并不等于已经独立验证了反证。

CaDiCaL 3.0 还提供了面向假设的传播与已推出文字查询接口。论文明确区分这些已发现的后果与全部逻辑后果：即使得到一些被迫文字，也不意味着已经找到模型或完成 UNSAT 判定。这一接口可以作为后续使用传播能力的入口，不能与本文只返回三种求解状态的基础流程混淆 \[[4, sec. 5](https://shijin.space/knowledge/sat-incremental-solving/index.md#ref-sat-incremental-solving-PollittEtAl2026Cadical)\]。

## 从编码到业务解释

一个完整的调用过程应保留变量与业务含义的映射，并把每次假设集合与结果配对。得到 SAT 时，检查完整编码与当前假设，再将业务变量解释成排班；得到 UNSAT 时，说明冲突涉及哪些背景约束和可选要求，需要时附上可检查的证明；得到 UNKNOWN 时，仅记录尚未解决。

这个小例子连接了专题中的几层内容：CNF 表达约束，CDCL 搜索模型或反证，传播与公式变换降低工作量，增量接口组织相关查询，最后由模型、核心和证明把结果交还给应用。

## 参考文献 {#references-sat-incremental-solving}

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

<div id="ref-sat-incremental-solving-MarquesSilvaLynceMalik2021CDCL" class="csl-entry">

1\. Joao Marques-Silva, Ines Lynce, and Sharad Malik. *Conflict-driven clause learning SAT solvers*. Handbook of satisfiability. 2021. [DOI](https://doi.org/10.3233/FAIA200987).

</div>

<div id="ref-sat-incremental-solving-SATCompetition2020IPASIR" class="csl-entry">

2\. SAT Competition 2020 Organizers. *IPASIR: Generic incremental SAT API*. 2020. [原文](https://satcompetition.github.io/2020/downloads/ipasir.h).

</div>

<div id="ref-sat-incremental-solving-BiereEtAl2024Cadical" class="csl-entry">

3\. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. *CaDiCaL 2.0*. Computer aided verification. 2024. [DOI](https://doi.org/10.1007/978-3-031-65627-9_7).

</div>

<div id="ref-sat-incremental-solving-PollittEtAl2026Cadical" class="csl-entry">

4\. Florian Pollitt, Mathias Fleury, Katalin Fazekas, Nils Froleyks, André Schidler, Dominik Schreiber, and Armin Biere. *CaDiCaL 3.0*. 29th international conference on theory and applications of satisfiability testing. 2026. [DOI](https://doi.org/10.4230/LIPIcs.SAT.2026.40).

</div>

</div>

## 配套演示

- [使用 SAT：从约束建模到可信结果 · 16:9](https://shijin.space/slides/sat-usage/index.html)
- [使用 SAT：从约束建模到可信结果 · 4:3](https://shijin.space/slides/sat-usage/index-4-3.html)