归结宽度

子句 $x_1\vee \cdots \vee x_k$ 排除的只是让这 $k$ 个文字全部为假的局部赋值。窄子句描述小范围冲突，宽子句同时协调许多变量。若一个公式的局部约束彼此都相容，而矛盾只在许多约束合并后显现，任何归结反驳都可能被迫经过一个宽子句；这个瓶颈可以用组合游戏、扩张性质或随机限制证明。

归结一步最多把两个前提除 pivot 外的文字合并，因此宽度可能增长，也可能因重合而下降。宽度小不意味着证明短：可有大量不同的窄子句。反过来，一个短证明不可能到处异常宽而毫无结构，因为宽子句可以在某些条件下被重新组织；Ben-Sasson–Wigderson 的权衡正把这种直觉变成定量结论。

再次考虑四子句公式

四个初始子句宽度均为 $2$。以前两项归结得 $y$，以后两项归结得 $\mathrm{\neg }y$，最后导出 $\mathrm{\perp }$，各行宽度依次为

所以这份证明宽度为 $2$。又因初始子句必须计入，$W(F)\ge w_0(F)=2$，从而可手算得到 $W(F)=2$，而不是仅给出一个上界。

宽度对编码非常敏感。把一个长子句用 Tseitin 辅助变量拆成 3-CNF 会把初始宽度降到 $3$，却增加变量和子句；新公式的 $W(F)$ 不能与原公式数值直接比较。子句若同时含 $u,\mathrm{\neg }u$，它是永真子句，按集合口径宽度虽为 $2$ 或更多，却可删除且不帮助反驳。重复写同一文字也不应人为抬高宽度。

还要区分 width 与 clause space。前者是一行的文字数，后者是验证过程中同时保留的子句数；总存储大致受二者乘积影响，却没有一个指标可替代另一个。对 XOR、基数约束等非 CNF 原语，必须先说明如何编码为子句，否则“宽度”尚未定义。

归结规模—宽度权衡公理库归结的规模—宽度权衡Resolution size-width tradeoff · Ben-Sasson–Wigderson theorem将一般归结的短证明转化为窄证明，并把宽度瓶颈转换为规模下界。说明：若最小宽度比初始宽度高出线性量，而变量数同阶，则最小 DAG 归结规模呈指数增长。于是研究者常先用扩张图、pebble game 或局部一致性证明宽度下界，再把它转换成长度下界。这个路线避开了直接追踪证明中每个可能子句。

宽度也具有算法含义。固定宽度上限 $k$ 时，至多有 $\sum _{i\le k}{2}^i(\genfrac{}{}{0ex}{}{n}{i})$ 个非永真子句；可以闭包枚举所有宽度不超过 $k$ 的 resolvent，并检查是否得到空子句。对常数 $k$ 这是多项式时间，但当最小宽度随 $n$ 增长时，枚举量迅速爆炸。该算法决定“是否有窄反驳”，并不自动找到接近最短的任意宽度证明。