树形归结

树形证明像一段没有 memoization 的递归程序。某个中间结论即使在两个分支都需要，也必须各算一遍；证明树不会保存一个节点供多个调用者引用。从根向叶反读时，每次 pivot 都把当前目标分成两个条件分支，这与回溯式 SAT 搜索的决策树很接近。相反，学习到的公共冲突子句若能跨分支复用，就自然产生 DAG。

“树形”不表示每个变量只分支一次，也不表示子句宽度小。沿不同路径可以反复选择同一变量；一个内节点也可能含很多文字。它只规定证明依赖的拓扑形状。因此树深、树大小、子句宽度是三个独立资源：平衡树可有对数深度而节点很多，窄子句也可能因重复推导形成巨大树。

令

前两项归结得 $x$。若允许共享，可分别用 $x$ 与 $\mathrm{\neg }x\vee y$、$\mathrm{\neg }x\vee z$ 得到 $y,z$，再由 $y$ 与 $\mathrm{\neg }y\vee \mathrm{\neg }z$ 得 $\mathrm{\neg }z$，最后与 $z$ 导出空子句。树形版本不能让同一个 $x$ 节点拥有两个父使用者，必须把

在 $y$ 分支和 $z$ 分支各写一次。这个小例只增加一次推理，却准确展示共享被禁止的位置；在递归依赖层层叠加的公式族上，重复可累积成指数差距。

树形限制应施加于子句实例。若只按文字集合去重，两个独立叶上同名的初始子句会被错误合并，树立即变成 DAG。反过来，把一份 DAG 逐路径展开总能得到树形证明，但输出大小可能按路径数爆炸，所以“语义上都能反驳”不等于多项式模拟。对 DPLL 的对应也需固定模型：纯回溯、是否允许 clause learning、restarts 和动态子句删除都会改变所对应的证明系统。

任何树形证明都可原样登记为 DAG 证明，故 DAG 归结以线性翻译 p-模拟树形归结。反向的直接展开没有多项式保证；确有显式公式族展示一般归结相对树形归结的指数级优势，但结论依赖具体大小度量和公式族，并不是从“图看起来更紧凑”一句话自动推出。近最优分离结果把这种重复计算现象定量化。

树形归结是分析无学习回溯搜索的标准桥梁。对给定变量分支树，每个叶若被某个初始子句证伪，可自底向上解析两个子树的冲突子句，得到树形反驳；反向也可从证明提取搜索结构。这个联系让证明大小下界转化为一类算法运行时间下界，但只约束与该证明模型吻合的算法，不能据此排除使用学习、代数推理或更强预处理的 SAT 求解器。