归结的规模—宽度权衡

每个顶点约束只涉及少量边；全局矛盾来自所有电荷的奇偶和。证明逐行合并局部信息时，必然出现一行，需要大约三分之一到三分之二的顶点约束才能推出。这样一个顶点集合向外暴露的每条边，都必须出现在这一行里；否则尚未提及的边还可以吸收奇偶差异。

扩张保证这个中间集合具有线性多条割边，于是中间子句很宽。规模—宽度定理再说明：如果整份证明短，就应存在另一份窄证明，与已经证明的宽度下界矛盾。这个下界允许 DAG 中间结论被反复复用；它没有把一般归结误当成不能共享的树形归结。

从约束依赖到宽度瓶颈 ​

依赖规模是次可加的 ​

对任意子句 $C$，定义

全部顶点约束不可满足，故这个最小值总存在。永真子句的 $\mu$ 为零；每个初始子句由单个 $P_v$ 推出，且不是永真式，所以 $\mu =1$。

若 $C$ 由 $A,B$ 一步归结得到，分别取推出两前提的最小顶点集，则其并集同时推出 $A,B$，由归结可靠性也推出 $C$。于是

如果允许 weakening，即从子句推出它的超集，$\mu$ 只会不增。这些性质对任意 DAG 的拓扑行序都成立。

最小依赖集合的每条割边都必须被提及 ​

设 $C$ 不是永真子句，$U$ 达到 $\mu (C)$。记 $S$ 为 $C$ 中的变量集合，$\alpha$ 为恰使其所有文字为假的唯一 $S$ 上赋值。因为 $P_U\models C$，在线性方程组 $P_U$ 中固定 $S=\alpha$ 后，剩余方程组在 ${\mathbb{F}}_2$ 上无解。

在 ${\mathbb{F}}_2$ 上，行化简理路行化简Row reduction用初等行变换把矩阵化为阶梯形以求解线性方程组和判定秩。只需行交换与行相加；无解意味着最终出现一行 $0=1$。追踪这行的来源，得到非空 $U^{\prime }\subseteq U$：把这些原始顶点方程异或后，所有未固定变量的系数都消失。图中内部边出现两次，只有割边出现一次，因此

式 (5) 表明，仅有 $P_{U^{\prime }}$ 就已排除 $C$ 的全部置假赋值，故 $P_{U^{\prime }}\models C$。$U$ 的基数最小，而 $U^{\prime }\subseteq U$，只能有 $U^{\prime }=U$。因此

对空子句使用同一论证，此时 $S=\varnothing$，所以 $\delta (U^{\prime })=\varnothing$。连通性迫使非空的 $U^{\prime }$ 等于 $V$。因此任何真子集的顶点约束都相容，且

这一步解释了连通性承担的任务：全局矛盾不能藏在一个更小的独立连通分量里。

每份反驳都要穿过中间规模 ​

沿证明行序，取第一行满足 $\mu >2N/3$ 的子句。式 (7) 保证它存在；初始行的 $\mu =1\le 2N/3$，weakening 也不可能首次跨过阈值，所以它来自两个较早前提的归结。

两前提的 $\mu$ 都至多 $2N/3$。由 (4)，至少一个前提的 $\mu$ 大于 $N/3$。取这个前提的最小依赖集 $U$，再用 (6)，就得到式 (2)。永真子句的 $\mu =0$，不会充当这个瓶颈。证明允许 weakening，也不要求所有输入子句都被使用。

K₄：16 个初始子句与精确宽度四 ​

取 $V=\{1,2,3,4\}$，以

标记六条边；电荷为 $(1,0,0,0)$。以下表格每一项都是一个完整子句，符号 $\mathrm{\neg }$ 表示否定。

平衡顶点集必须恰有两个顶点，割边数都是四，故式 (2) 给 $W\ge 4$。例如 $U=\{1,2\}$ 的割边为 $\{b,c,d,e\}$；合并其方程得到 $b\oplus c\oplus d\oplus e=1$，而补集 $\{3,4\}$ 要求同一组割边的异或为零。

完整 47 行反驳证书 ​

记 $D_{\beta }={\ell }_b({\beta }_b)\vee {\ell }_c({\beta }_c)\vee {\ell }_d({\beta }_d)\vee {\ell }_e({\beta }_e)$，其中 $\beta$ 按 $b,c,d,e$ 排列。下面列出全部 16 个四元子句的两个父行和 pivot；每行都是一次标准归结。

例如第 22 行把 $\mathrm{\neg }a\vee b\vee \mathrm{\neg }c$ 和 $a\vee d\vee \mathrm{\neg }e$ 在 $a$ 上归结，得到 $b\vee \mathrm{\neg }c\vee d\vee \mathrm{\neg }e=D_{0101}$。余下每一行由下表的编号规则唯一指定：$j$ 从零开始，结果按剩余变量的赋值字典序排列。

这份证书有 16 个初始行、31 次推理，最大宽度为四。因此 $W(T(K_4,\chi ))=4$，且 $S\le 47$；没有声称 47 是最短规模。第 17–32 行的最小依赖规模为二，正是一般证明中的中间瓶颈。代入式 (1) 时 $W-w_0-1=0$，得到的规模下界仍平凡；小图验证机制，指数结论则来自整个固定度数扩张图族。

编码与证明系统的边界 ​

奇偶矛盾式有多项式时间的线性代数判定方法，上面的全体方程一异或便得到 $0=1$。困难的是指定 CNF 在归结系统中的证明规模，不是求解这些线性方程本身。允许直接异或整条方程的证明系统具有不同的推理能力。

这里的 Tseitin 图矛盾式也不同于把任意布尔电路转成 CNF 的辅助变量变换。重新编码会改变变量数、初始宽度和可用中间命名；旧公式的 (2) 不会自动适用于新编码。类似地，tree-like size、regular resolution、proof space 都需要自己的比较定理。

式 (3) 展示了一条可以逐项检查的下界路线：每顶点常数多个 CNF 子句、边变量总数线性、最小依赖集合的割边线性，最后才是指数规模。若缺少变量数或初始宽度的控制，单说“宽度线性”不足以推出同一规模界。

随机限制下的归结下界理路随机限制法的归结下界Random-restriction resolution lower bound · Restriction method for resolution用随机部分赋值压缩假设中的短归结证明，同时保留受限公式的组合困难性。沿另一方向利用宽度：限制假设中的短证明，同时保存受限公式的困难性。本页的图上宽度证明本身是确定性的；它可以作为其他证明中要保存的困难结构。规模—宽度定理提供长度下界，并未提供寻找最窄或最短反驳的高效算法。