We establish exact formulas for the minimum DPLL refutation tree size (with unit propagation) of two fundamental families of unsatisfiable Boolean formulas. For Tseitin formulas on any connected graph G with cycle rank f = |E|−|V|+1, we prove DPLLBT (Tseitin (G) ) = 2^f+1 − 1. For pigeonhole formulas, we prove DPLLBT (PHP (p, p−1) ) = 2 (p−1) ! − 1. We introduce an efficient translation from DPLL trees to tree-like Resolution proofs: the Bridge theorem, SIZE (Rₑff (T) ) = DPLLBT (T) + 2·UP (T), yields proof sizes depending on a unit propagation count UP (T) whose variability across orderings was previously uncharacterized. We resolve this by proving the Cascade Constancy Theorem: for cotree-first DPLL on Tseitin formulas, the number of variables forced by unit propagation at each depth level depends only on the graph structure and cotree ordering, not on the branch values. This gives an exact closed-form formula UP (T_π) = Σ 2ᵈ · c_π (d), where c_π (d) is the cascade function computable in polynomial time from G and π. All results are computationally verified.
Aliaksei Naboko (Sat,) studied this question.