归结反驳

一条归结推理消去一个二择变量。第一前提说“若 $x$ 为假，就必须靠 $C$”；第二前提说“若 $x$ 为真，就必须靠 $D$”。不论怎样选择 $x$，剩余赋值都要让 $C$ 或 $D$ 成立，所以可以把 $x$ 从结论中消去。反驳不断压缩所有可能分支，直到得到没有任何文字可挽救的空子句。

这种局部性既是力量也是限制。验证者只需比较两行和一个 pivot，归结因而非常适合 SAT 求解器的冲突证书；但每行只能表达一个析取子句，无法像一般 Frege 证明那样把任意嵌套公式作为中间引理。证明复杂度下界正是量化：一个不可满足公式虽没有模型，要让这种单一行语言暴露矛盾，可能需要多少子句、多少宽度或多少次重复推导。

考虑

前两项以 $x$ 为 pivot 归结得单位子句 $y$；后两项归结得 $\mathrm{\neg }y$；再以 $y$ 归结得到空子句：

这是三次推理、最大子句宽度为 $2$ 的可手检反驳。它也说明方向：归结证明的输入是不可满足 CNF，输出不是某个“假赋值”，而是从所有子句推出矛盾。相应的永真式是 $\mathrm{\neg }F$；把 $F$ 自身误称为被证明的永真式会倒置语义。

完备性可按变量消元理解：选变量 $x$，保留不含 $x$ 的子句，把所有含 $x$ 的子句与含 $\mathrm{\neg }x$ 的子句两两归结，再删去含 $x$ 的原子句。对剩余变量的每个赋值，所得公式恰好判断原公式能否通过选择 $x$ 扩展为满足赋值。若扩展的 $x=0$ 和 $x=1$ 都失败，就有一对前提的其余文字同时为假，其归结式也为假；反之，归结式全真便不会同时出现两种冲突要求。逐变量消元后，不可满足性只能表现为空子句。这个过程可能产生指数多子句，所以完备性没有给出短反驳。

归结完备性依赖先把公式放进 CNF。Tseitin 编码引入辅助变量后通常只保持等可满足性，而非原变量上逐赋值同值；证明长度比较必须把编码规模计入。不同定义可能允许 weakening、删去永真子句或把同一子句重复登记，这些约定通常可多项式互译，却会改变精确的行数。对子句数的下界若不声明计数节点、推理步还是总文字数，也没有可复核含义。

树形归结公理库树形归结Tree-like resolution每个导出子句至多被后续一步使用、因而证明依赖图为树的归结限制。禁止共享已导出子句，DAG 形归结公理库DAG 形归结DAG-like resolution · General resolution允许已导出子句被多个后续步骤共享的一般归结证明表示。允许一个引理被多次引用；二者使用同一局部规则，却有不同的全局资源。归结宽度公理库归结宽度Resolution width · Clause width in resolution以证明中最大子句文字数衡量归结反驳所需的局部表达宽度。记录反驳中最宽的子句，规模—宽度权衡公理库归结的规模—宽度权衡Resolution size-width tradeoff · Ben-Sasson–Wigderson theorem将一般归结的短证明转化为窄证明，并把宽度瓶颈转换为规模下界。把某些宽度下界转成长度下界。这些指标共同解释为什么“规则只有一行”仍能产生精细的复杂度层次。

现代 CDCL SAT 求解器的冲突分析和 clause learning 可输出归结式证书；带 restart 的理想化 CDCL 与一般归结之间存在多项式模拟结果，但具体结论依赖学习方案、分支规则与是否允许擦除。工程求解速度也不等于短归结证明：预处理、扩展变量、异或推理或专用理论传播可能已经越出纯归结模型，认证时必须把这些步骤展开或交给更强的证书格式。