DAG 形归结

DAG 形证明相当于给递归论证加入缓存。第一次推出引理 $C$ 后，任何后续分支都可以引用节点编号而不重做 $C$ 的全部祖先。一个短证明因而可以把局部矛盾压缩成可重用的 clause，逐步建立一张冲突知识库。现代 SAT 求解中的 clause learning 正是这种思路的算法化版本，不过实际求解器还涉及学习子句选择、遗忘、restart 与预处理，不能不加条件地与某个静态 DAG 完全等同。

共享只压缩重复结构，不会让错误推理变真。每个非源节点仍需由两个已出现子句和一个 pivot 局部验证；拓扑序排除了循环论证。若允许节点引用自己或未来节点，验证者就不能用简单归纳保证每行都是初始 CNF 的逻辑后果，因此“有向无环”不是绘图偏好，而是可靠性证明的一部分。

对公式

建立节点序列

$C_6$ 的出度为 $2$，整份证明只推导一次 $x$。逐条代入即可核对五次推理；树形展开则必须复制产生 $C_6$ 的两叶子证明。这个例子展示压缩机制，却不能用常数差距证明渐近分离；渐近结论需要一个随参数增长的公式族和严格计数。

若按上述编号计，证明有五个初始节点、五个导出节点和十条父引用边；若只计推理步则大小为五。两种数值都正确，但必须随定义报告。把同一子句 $x$ 在表格中抄写两行而仍让两行引用同一个祖先，不会恢复树形性；判断标准是依赖边，不是打印文本是否重复。

允许共享也不等于允许 extension variable。DAG 节点只能保存由归结推出的子句，不能随意为一个大公式命名。若加入新变量及定义子句，得到的是扩展归结等更强模型，输入编码与可靠性条件随之改变。另一个边界是 clause deletion：从静态证书中删去不再使用的节点不会改变可证性，但在线求解时删除过早会影响未来搜索，空间复杂度需另行计量。

一般所说的 resolution size 下界通常针对 DAG 形归结，因为它允许最充分的子句复用；这样的下界自动适用于受限的树形系统。归结宽度公理库归结宽度Resolution width · Clause width in resolution以证明中最大子句文字数衡量归结反驳所需的局部表达宽度。与规模—宽度权衡公理库归结的规模—宽度权衡Resolution size-width tradeoff · Ben-Sasson–Wigderson theorem将一般归结的短证明转化为窄证明，并把宽度瓶颈转换为规模下界。也以一般归结为主要口径：即使 DAG 可以共享，若任何反驳都必须经过很宽的“瓶颈子句”，证明仍会被迫拥有很多不同节点。

从算法角度，DAG 证书可用父行索引流式检查，并通过引用计数释放不再需要的子句；这区分了证明大小与 proof space。一个证明可能节点总数很大但任一时刻只保留少量子句，也可能很短却需要同时保存多个宽引理。共享解决的是时间式重复，不自动解决内存、宽度或寻找下一条引理的难题。