Exact DPLL Complexity and an Efficient Bridge to Tree-like Resolution

We establish exact formulas for the minimum DPLL refutation tree size (with unit propagation) for Tseitin formulas and pigeonhole formulas. For Tseitin formulas on any connected graph G with cycle rank f, we prove DPLL_BT(Tseitin(G)) = 2ᶠ⁺¹ − 1. For pigeonhole formulas, we prove DPLL_BT(PHP(p,p−1)) = 2(p−1)! − 1. We introduce an efficient DPLL-to-Resolution translation that defers unit propagation resolution to internal nodes, yielding the Bridge theorem: SIZE(R_eff(T)) = DPLL_BT(T) + 2·UP(T). All results are computationally verified on 21,096 DPLL trees across 7 graph families.