回到学习路线。本练习用一个可满足公式和一个不可满足公式，分别交付原模型与反驳证据。两个出口都要回到最初输入，不能只报告中途检查成功。

下载标准库核验器。运行 python foundation-cnf-repair-rat-check.py；用 python -O 重跑应得到完全相同的JSON。程序只写标准输出，使用显式检查；其中固定小实例和有限穷举只用于复算本文，Python程序本身未在证明助理内形式化验证。

一、先删三条子句，再交一个原模型 ​

变量为 $b,c$，在程序中编码为1、2，负数编码否定。输入编号为

任务是执行阻塞子句消除理路阻塞子句消除Blocked clause elimination · BCE按阻塞文字删除CNF子句，保存逆序修复栈，将简化模型恢复为原模型，并以冻结变量保留指定输入的存在扩张。，输出删除顺序、每条pivot、最终公式与反向恢复后的总赋值。不能把“没有剩余子句”直接当成已经交付原模型。

第一条候选1不能删：以 $b$ 和3归结只剩 $(c)$，以 $c$ 和2归结只剩 $(b)$。子句2可以由 $b$ 阻塞，因为唯一反pivot子句3给出 $\mathrm{\neg }c\vee c$。删2之后，子句1可以用纯文字 $c$ 删除；最后删3，pivot选 $\mathrm{\neg }b$。

因此日志在程序的整数编码中是 ((2,1),(1,2),(3,-1))，最终公式为空。选择简化模型 $b=c=0$，逆序执行：

1. 恢复3：$\mathrm{\neg }b$ 已真，保留00
2. 恢复1：全假，令 $c=1$，得到01
3. 恢复2：全假，令 $b=1$，得到11

把11带回原式，三条都真。输出 sat.recovered 为 [true,true]，sat.repairs 的翻转标志依次为 false,true,true。

迁移：把同一日志按正序恢复。 从00开始，2先由 $\mathrm{\neg }c$ 满足，1使 $c$ 变1，3又由 $\mathrm{\neg }b$ 满足，于是停在01。这时2全假，程序的 forward_wrong 正是这个反例。用单步翻转引理解释：后来删除的pivot只承诺保护其删除时仍活动的子句，不承诺保护更早已经删除的子句。

二、保留下一次查询的含义 ​

原公式只有模型11；简化为空式后有00、01、10、11四个模型。恢复映射把它们送回原模型，但不会保留每一位。因此，如果下一次查询添加假设 $b=0$，不能先用空简化式说“有解”，再把 $b$ 改成1交差。

将 $b$ 冻结，要求删除pivot不得是 $b$ 或 $\mathrm{\neg }b$。重新执行，唯一删除记录为 (3,2)：子句3以 $c$ 为pivot，其和2的归结式为 $\mathrm{\neg }b\vee b$。剩下1、2，两条共同迫使 $b=1$，所以假设 $b=0$ 仍无解。

请分别列出冻结 $P=\varnothing$、$P=\{b\}$、$P=\{b,c\}$ 时的结果。第三种不允许任何pivot，所以三条原子句全部保留。证明一般投影结论时，不需要数完全部模型：反向恢复只翻非冻结变量，因此每个固定冻结赋值的“存在扩张”在前后保持。

三、把反向修复依据交给RAT检查器 ​

从空数据库开始，按3、1、2加回原子句：

RAT(3, [not b,c], not b, [])
RAT(1, [b,c], c, [])
RAT(2, [b,not c], b, [(3,[])])

第一步没有正 $b$ 子句，第二步没有负 $c$ 子句，两个RAT检查的候选集合为空。第三步的唯一反pivot编号为3，中间子句是 $b\vee \mathrm{\neg }c\vee c$，全假假设已经矛盾，故不需传播提示。

RAT重放理路RAT子句证书检查RAT clausal proof checking · Resolution asymmetric tautology · RAT proof checking检查覆盖全部反pivot子句的RAT提示分支，以可满足性前向保持证明UNSAT，并区分局部传播、合法前缀与最终空子句。返回 VALID_PREFIX。它没有加入空子句，也没有证明UNSAT；恢复得到的11恰好证明当前公式可满足。这个任务将同一删除日志接到另一种接口，但不混淆两者的完成条件。

四、八子句反驳的四个分支都要交齐 ​

变量 $a,b,c$ 编码为1、2、3，输入为：

先独立核UNSAT：任取三位赋值，选择每位上那个为假的文字，表中总有完全由这三个假文字组成的子句。再检查以下证书，不把上述穷举论证当成提示的一部分：

RAT(9, [a], a, [(5,[1]),(6,[2]),(7,[3]),(8,[4])])
AT(10, [b], [9,5,6])
DEL([1,2,3,4,5,6])
AT(11, [], [9,10,7,8])

第一行的四个中间子句分别是1、2、3、4本身。它们各自全假时，用对应原子句作唯一提示即可冲突。每个分支的假设必须清空后重建，不是把四组不同的 $b,c$ 值塞进一张赋值表。

第二行从 $b=0$ 开始，依次传播 $a=1,c=1$，在6冲突。删除之后活动编号是7、8、9、10。最后一行没有额外假设，9和10传播 $a=b=1$，7传播 $c=1$，8冲突，加入编号11的空子句。最终 cube_proof.status 应为 UNSAT_CERTIFIED，活动编号为 [7,8,9,10,11]。

为什么第一行不能直接改为RUP？ 只假设 $a=0$ 时，5–8已满足，1–4都还有两个未定文字，没有单位可选。日志若写 AT(9,[a],[1])，检查器在非单位提示1处拒绝。RAT的能力来自分别核查四组更强的局部反证假设。

五、改动证据结构，定位首次拒绝 ​

• 漏掉分支8：三个剩余冲突都成立，但反pivot编号集合不完整，RAT行拒绝
• 某分支引用9：9是尚未通过检查的候选，引用不活动编号，拒绝
• 先删除1，再保留分支5的提示1：删除不会被缓存复活，拒绝
• 删除9后重新使用编号9：永久已用集合仍含9，拒绝
• 传播已经冲突后还写提示：违反“冲突是最后提示”的明确教学语法，拒绝
• 在两条相反单位子句的公式中直接删除它们：得到空子句集，仍只返回 VALID_PREFIX

再看一个可满足输入：1为 $\mathrm{\neg }p\vee q$，2为 $(q)$。RAT加入 $(p)$ 的唯一分支为 (1,[2])，却不能证明旧式蕴涵 $p$，因为 $(p,q)=(0,1)$ 是旧模型。用翻pivot修复到 $(1,1)$，说明整个证书应维护SAT存在性的前向保持，而非每个新子句都是原式逻辑后果。

身份迁移： 把上述编号1复制为另一活动编号，得到1和2都为 $\mathrm{\neg }p\vee q$，3为 $(q)$。加入编号4的 $(p)$ 时，必须同时给 (1,[3]) 与 (2,[3])。内容相同不等于同一身份；漏任一个仍应拒绝。下载器实测这一接受与拒绝，并总共执行20个非法输入拒绝例。

六、核清成本和能交付的结论 ​

BCE寻找pivot的参考器采用全表扫描，最多 $m$ 次删除；按 $m$ 条子句、$L$ 次文字出现计，保守时间为 $O(|P|+(m+1)(L+1)(m+L+1))$。已验证日志的核心模型恢复为 $O(n+m+L+1)$；完整 certify_sat 还重检日志，整体为 $O((m+1)(m+L+1)+n)$。这三个接口的成本不能互换。

RAT重放按每步活动表扫描、所有中间子句构造和所有提示所读的文字计费。下载器输出完整分支假设与单位/冲突日志，输出空间也必须收费；它没有把这些事件串假称成常数空间。

最后交付三项独立结果：原SAT实例的合法总模型、原UNSAT实例的完整接受证书、结构损坏日志的准确拒绝原因。被拒的日志不告诉我们原式真假；冻结变量之外的新增假设，也不在原预处理投影保证之内。