RAT子句证书检查

两种局部保证，两种全局不变量 ​

RUP像排除反例：“任何原模型都必须满足新子句。”RAT允许修正反例：“如果旧模型不满足新子句，把这一个pivot改成真，仍能保住所有旧约束。”因而不能沿用RUP的“每个活动子句都由原式蕴涵”不变量。

整个日志使用的保证是

它只要求一个原模型的存在能够沿合法操作持续下去。添加RAT有构造性模型修复保证；删除子句只减弱条件，也维持这个方向。最后若 $D$ 含空子句，它没有模型，于是反推 $F_0$ 没有模型。

为什么翻pivot不会弄坏旧公式 ​

先用旧RUP的局部可靠性：通过的AT检查说明 $D\models A_j$，因为假如总模型满足 $D$ 和 $\mathrm{\neg }{A}_j$，每次单位传播都必须与这个模型一致，不可能走到冲突。

取任意 $\alpha \models D$。若它已满足 $C$，直接保留。否则 $C$ 的全部文字在 $\alpha$ 下为假，特别是 $\ell$ 假。对每个含 $\mathrm{\neg }\ell$ 的 $D_j$，由 $D\models C\cup (D_j\setminus \{\mathrm{\neg }\ell \})$ 可知，$D_j$ 的余部在 $\alpha$ 下必有真文字。

把 $\ell$ 改真得到 ${\alpha }^{\prime }$。候选 $C$ 现在满足；上述余部不含pivot变量的另一极性，也不含 $\ell$，因为 $D_j$ 已拒绝重言，所以原有真文字未改变。其他不含反pivot的旧子句不会失去原有真文字。因此 ${\alpha }^{\prime }\models D\wedge C$，添加确实保持可满足性。删除则不需要给出被删子句的冗余证明；它可以让后续证明变难，却不会破坏SAT存在性的前向保持。

一个可满足例子直接区分RAT与蕴涵 ​

设编号1为 $\mathrm{\neg }p\vee q$，编号2为 $(q)$，准备添加编号3的 $(p)$，pivot为 $p$。唯一反pivot子句是1；中间子句为 $p\vee q$。令 $p=q=0$ 后，提示2立即冲突，所以RAT分支通过。

但旧模型 $(p,q)=(0,1)$ 不满足 $(p)$，旧公式并不蕴涵这个新单位子句。它也不是RUP：假设 $p=0$，传播 $q=1$ 后没有冲突。RAT证明允许把该模型改成 $(1,1)$，两条旧子句仍真。

这个新子句也不满足BCE的纯重言条件：和编号1按 $p$ 归结只得到 $(q)$，不是重言式。RAT可借助其他活动子句的传播证明安全，因而比“所有相关归结式字面上重言”更宽。

八个三文字子句的完整反驳 ​

用全部八种极性组合构造原式，顺序为：

每个总赋值恰好使其中一条全假，所以原式不可满足。单位传播在空赋值下看不到单位；只假设 $a=0$ 后，5–8已满足，1–4都只剩两个未定文字，仍没有传播。因此直接添加单位 $(a)$ 不满足RUP。

RAT却能验证它。以 $a$ 为pivot，反pivot候选恰是5、6、7、8。对应中间子句分别等于已有的1、2、3、4；把中间子句全赋假时，用同内容的原子句作唯一提示就立即冲突。完整记录为

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])

第二行假设 $b=0$，提示9传播 $a=1$，提示5传播 $c=1$，提示6冲突。最后一行没有反证假设：9、10分别传播 $a=b=1$，7传播 $c=1$，8冲突。此时才能以最后加入的空子句宣布原式UNSAT。

哪些改动必须拒绝 ​

删去第一行的分支8，剩余三个局部传播仍各自正确，但全反pivot集合没有覆盖，整行拒绝。把某分支提示改成9也拒绝：候选9还未加入，不能参加自己的论证。若先删除1，再沿用分支5的提示1，会在活动编号检查处拒绝。

若直接尝试 AT(9,[a],[1])，反证假设只有 $a=0$，子句1还含两个未定文字，不能传播。这是RAT有意义的地方：它的分支分别增加了 $b,c$ 的反证假设，而不是把同一非单位步骤换个名字就接受。

在可满足小例中只删除全部子句，或者完成合法RAT添加就停止，均只得到 VALID_PREFIX。被拒的日志也不证明原式可满足；它只说明这份候选证据没有通过既定接口。

反向子句消除为什么能加入日志 ​

阻塞子句消除理路阻塞子句消除Blocked clause elimination · BCE按阻塞文字删除CNF子句，保存逆序修复栈，将简化模型恢复为原模型，并以冻结变量保留指定输入的存在扩张。删除 $C$ 时，每个反pivot子句与它的普通归结式都含互补对。因此反向添加时，中间子句 $C\cup (D_j\setminus \{\mathrm{\neg }\ell \})$ 也含互补对，每个对应RAT分支只需空提示。

例如对三子句 $b\vee c$、$b\vee \mathrm{\neg }c$、$\mathrm{\neg }b\vee c$，按2、1、3删除后，可从空数据库按3、1、2加回。前两步没有反pivot候选；最后一步以 $b$ 为pivot，唯一反pivot编号3的中间子句为 $b\vee \mathrm{\neg }c\vee c$，字面重言。整个前缀合法，却没有任何UNSAT结论。这让同一模型修复依据同时成为可检查的添加依据。

检查成本要数扫描、分支与提示文字 ​

采用期望常数时间的散列表，令输入与记录的总编码项目数为 $I$；每个RAT步骤检查时有 $m_t$ 条活动子句。记 $B$ 为所有RAT中间子句构建前的文字数之和，$H$ 为所有实际提示读取的 $1+|D(h)|$ 之和。候选子句读取、AT初始赋值和分支/记录表头都计入 $I$；空子句也有表头。

本页程序完整扫描当前数据库以核对反pivot集合，再按各分支重新建立假设，所以接受一份有限日志的期望时间为

它没有从提示格式凭空取得“只看提示、不扫数据库”的保证。记录可以删除大量子句后继续，也可以不断增加新的永久编号；额外空间必须分别计当前活动文字、全部已用编号、最大单次局部赋值，以及审计输出。

审计输出保留每个中间子句的全假假设和单位/冲突事件，长度按 $O(I+B+H+1)$ 上界计；关闭输出才可省下这一部分。编号/文字超出单位字长时，字典操作和整数比较还应增加位成本。有限循环保证检查终止，但资源不足只能返回未完成或拒绝，不能省略剩余分支后默认通过。

信任边界仍从原式开始 ​

RAT缩小的是求解器日志验证责任，不能修正上游的错误CNF编码。若程序性质少编码了一个约束，可靠检查器也只会证明它实际收到的公式。本文的Python参考器使用显式检查，在普通与 -O 模式执行同一验收；这不是在证明助理内验证过的生产LRAT内核。[1]中的Coq/ACL2实现承担更强的形式化验证任务。

综合练习交付完整删除日志、SAT模型恢复、四分支RAT反驳与错误日志拒绝。迁移时增加一个同内容但新编号的反pivot子句，必须同时增加其分支；只比较子句内容集合会漏掉本页的身份合同。