阻塞子句消除

阻塞文字不是必然为真的文字 ​

一条子句可以靠多个文字满足。假如现在它全假，指定的 pivot 就是一只可以安全拨动的开关。与它相反的文字可能原本帮其他子句取真，因而不能只说“把这一位改好就行”；阻塞条件逐条检查那些可能受伤的子句，保证每一条都藏着另一项真文字。

这也说明为何要保存删除时刻的理由。较早删除的子句在后续步骤中已经不参与阻塞检查；后来选出的 pivot 未必能保护它。恢复必须沿相反顺序，使每次翻转面对的，恰是那次删除时仍需保护的约束。

先找删除点，再消费修复栈 ​

下载程序的 eliminate 按活动编号顺序扫描子句，再按输入的文字顺序寻找第一个非冻结阻塞文字。找到后删除一条并重新扫描。它不调用SAT判定器，也不靠某个试验赋值决定是否可删。每次成功删除都让活动子句数减少一，最多删除原有的 $m$ 条。

replay_bce 接受外部删除日志时重新检查：编号当前活动、pivot确实属于子句、变量未冻结、全部反pivot候选都通过。它返回经过验证的修复栈。restore 的前提是使用这个栈，并接收定义在整个原变量域上的总赋值；简化式不再提到的变量仍可先任意填值。

恢复从栈顶往下走：已满足的子句直接跳过，全假的子句才把记录的 pivot 置真。归纳不变量是“当前模型满足已恢复的全部子句及最终剩余式”。翻转引理维持它；栈耗尽时得到原公式模型。完整 certify_sat 还会重新扫描原公式核验最终赋值。

三个子句，两次必要翻转 ​

取 $V=\{b,c\}$，$P=\varnothing$，编号如下：

初始两个变量都以两种极性出现，没有纯文字。$C_1$ 的两个 pivot 都失败：以 $b$ 和 $C_3$ 归结得到 $(c)$，以 $c$ 和 $C_2$ 归结得到 $(b)$，都不是重言子句。$C_2$ 却由 $b$ 阻塞：唯一含 $\mathrm{\neg }b$ 的 $C_3$ 给出 $\mathrm{\neg }c\vee c$。

先删 $(C_2,b)$。此时 $\mathrm{\neg }c$ 消失，$C_1$ 中的 $c$ 成为纯文字，故再删 $(C_1,c)$。最后删 $(C_3,\mathrm{\neg }b)$，得到空子句集。原公式唯一模型是 $(b,c)=(1,1)$；空子句集却接受全部四个赋值。

选择最容易写下的简化模型 $(0,0)$，逆序恢复：

最后三个原子句分别至少有 $b,b,c$ 为真。若错误地正序恢复，第一步 $C_2$ 已由 $\mathrm{\neg }c$ 满足，第二步把 $c$ 改成1，第三步又由 $\mathrm{\neg }b$ 满足，于是停在 $(0,1)$，恰好弄坏已经检查过的 $C_2$。

冻结查询变量，避免把假设改掉 ​

假设应用随后要问原公式在 $b=0$ 下是否有解。若只保存不受限制的空简化式，答案会误变为有解；恢复算法最终把 $b$ 改成1，不能算满足原查询。一次性的等可满足预处理不会自动支持以后追加任意假设。

把 $b$ 放入 $P$ 后，$C_2$ 的 $b$ 不能用作删除pivot。扫描会改为删除 $C_3$，其 $c$ 与 $C_2$ 的归结式为 $\mathrm{\neg }b\vee b$。剩余 $C_1\wedge C_2$ 不再允许删除，且仍迫使 $b=1$。任意剩余模型均可只改 $c$ 恢复，因此查询 $b=0$ 仍正确得到无扩张。

一般地，对每个固定的 $\pi :P\to \{0,1\}$，都有

这是冻结pivot限制加上翻转引理的直接推论。它允许对冻结变量追加任意布尔约束，不能保证在非冻结变量上追加约束也安全。模型计数同样要谨慎：上例从一个模型变成四个，重构函数可以把多个简化模型送到同一个原模型。

一个漏检就足以弄坏恢复 ​

对 $F=(b)\wedge (\mathrm{\neg }b\vee c)$，子句 $(b)$ 不能由 $b$ 阻塞，因为归结式为 $(c)$。若漏掉唯一反pivot子句而错误删除它，$(b,c)=(0,0)$ 满足剩余式；修复把 $b$ 置1之后，$\mathrm{\neg }b\vee c$ 变假。这与合法例中的互补保护形成逐项对照。

穷尽删除的剩余式唯一，恢复的模型可以不同 ​

删除其他子句只会减少一个阻塞检查需考虑的反pivot候选，不会让已经有效的阻塞文字失效。因此同一固定 $P$ 下，任意穷尽删除顺序都到达相同的剩余子句集。[1, §4]

可以不借助额外定理证明这个结论。取两个终态 $A,B$，按产生 $B$ 的删除顺序考察每条子句。假设此前被删的子句在 $A$ 中也都不存在。如果本条仍在 $A$，那么 $A$ 是其删除时活动式的子集，它在 $A$ 中仍被同一非冻结文字阻塞，与 $A$ 已终止矛盾。所以产生 $B$ 时删除的每条子句也都不在 $A$，得 $A\subseteq B$；交换两序列再得反包含。

该结论说的是剩余公式，不是删除日志或所选模型。改变pivot、初始简化模型或恢复次序中的合法选择，可能得到不同原模型；所有输出仍须逐子句满足原式。

把搜索、验证和恢复的费用分开 ​

设输入有 $n$ 个声明变量、$m$ 条子句、$L$ 次输入文字出现（含随后合并的重复文字），散列表查询按期望常数成本计。单次固定 $(C,\ell )$ 检查扫描全部活动子句，并在反pivot子句中找跨集合的互补项，时间 $O(m+L+1)$。程序不实际反复拼接归结式，因而无需每检查一个 $D$ 就复制整份 $C$。

一轮最多尝试 $L$ 个pivot并检查 $m$ 个表头，成功删除至多 $m$ 次。因此参考器的全部寻找过程有保守界

这不是高性能SAT预处理器的索引界。公式与修复栈的文字存储为 $O(m+L+1)$；冻结变量表另计 $O(|P|+1)$。已验证栈上的恢复加前后模型扫描为 $O(n+m+L+1)$ 时间，输出模型占 $O(n)$，修复事件只记录编号、pivot和是否翻转，不复制整张赋值表。

公开 certify_sat 还先重放外部日志，至多做 $m$ 次固定pivot检查，所以其整体上界为 $O((m+1)(m+L+1)+n)$，不能把核心恢复的线性界直接当成整个认证接口的成本。整数编码超过机器字时，编号和散列等操作另计位成本。

接到完整的双出口任务 ​

对SAT结果，保留并验证删除日志，再恢复原模型。对UNSAT结果，若简化式已有可靠反驳，因为它是原式的子集，原式也不可满足；只有删得很短却没有模型或反驳，仍不能宣布答案。

反向加入一条被BCE删去的子句，也是RAT证书理路RAT子句证书检查RAT clausal proof checking · Resolution asymmetric tautology · RAT proof checking检查覆盖全部反pivot子句的RAT提示分支，以可满足性前向保持证明UNSAT，并区分局部传播、合法前缀与最终空子句。可检查的一步：每个反pivot的非pivot余部已经提供互补对。沿删除日志反向加入可以得到合法前缀，但合法前缀不自动构成UNSAT证书。

综合练习要求复算上述三个删除和两次翻转，冻结 $b$ 后重新求终态，再核验三变量八子句的RAT反驳。最后去掉一个反pivot分支，定位检查器第一次拒绝的位置。