归结的规模—宽度权衡

假设已有一份很短却含宽子句的证明。证明行总数不多，便可以寻找一个适当的部分赋值，把宽子句大多满足或压窄，同时让初始公式仍保留足够矛盾。对受限证明做清理，会得到一份更窄的反驳。反复组织这一思想可推出：短证明必然能够“窄化”。因此若独立的组合论证表明任何反驳都必须经过宽度瓶颈，短证明假设就无法成立。

这一定理强在把一个全局计数问题变成局部表达问题。直接证明 DAG 中必须出现指数多个节点，需要控制可能的共享方式；证明宽度下界只需说明所有窄子句仍不足以表达全局矛盾。代价是平方除以 $n$：宽度增量只有 $O(\sqrt{n})$ 时，所得规模下界可能只是常数级，不能把任何非零宽度差都宣传成指数下界。

四个二元子句

有 $n=2$、$w_0=2$，并存在宽度 $2$、三次推理的反驳，所以 $W-w_0=0$。代入下界只得 $S\ge \exp (\mathrm{\Omega }(0))$，即一个平凡常数；这与短证明一致。这个计算提醒我们，定理不是用来重新证明每个小公式都困难。

真正产生指数下界的机制是一个公式族 $F_n$：若编码使用 $\mathrm{\Theta }(n)$ 个变量、初始宽度有固定上界 $k$，而组合论证给出 $W(F_n)\ge \alpha n$，那么

故 $S(F_n)=\exp (\mathrm{\Omega }(n))$。每一项的增长来源都清楚可查；仅写“宽度是线性的所以指数”而不说明变量数和初始宽度，可能在辅助变量编码下得到错误结论。

定理针对一般 resolution 的标准大小。对 tree-like size、regular resolution、proof space 或总系数位数，需使用相应权衡，不能直接替换符号。它给的是最坏情况下界，未提供寻找最窄证明的高效算法；计算 $W(F)$ 本身仍可能困难。

Tseitin 矛盾式、随机 CNF 和若干基于扩张图的公式族具有强宽度下界，因而可沿此定理得到一般归结的指数规模下界。随机限制下的归结下界公理库随机限制法的归结下界Random-restriction resolution lower bound · Restriction method for resolution用随机部分赋值压缩假设中的短归结证明，同时保留受限公式的组合困难性。则提供构造或保存宽度瓶颈的一种常用机制：限制让假设中的短证明变窄，同时让剩余公式仍需要宽子句，两边相撞。

在 SAT 编码设计中，这个权衡也解释辅助变量的双重作用。它们能把长约束拆为窄初始子句，却同时增加 $n$，并可能为证明提供新的中间命名；因此仅比较两个编码的 clause width 无法预测求解难度。严谨比较应把 $w_0$、最小 $W$、变量数和翻译后的证明规模放在同一个不等式中。