DPLL and CDCL are the two dominant paradigms for SAT solving. DPLL explores the search tree by branching and backtracking. CDCL adds clause learning — when a contradiction is found, the solver derives a new clause explaining the failure and backtracks non-chronologically. In practice, CDCL dominates. But proving a formal separation — that CDCL is exponentially more powerful than DPLL on some family of instances — had remained open.
This paper provides the separation. A deterministic CDCL configuration using a VSIDS-like branching heuristic solves the Ordering Principle formulas in polynomial time, while any DPLL solver requires exponential time on these same instances. The Ordering Principle states that every finite partial order has a minimal element; its negation produces unsatisfiable CNF formulas that are notoriously hard for tree-like resolution.
The key is that CDCL's clause learning lets it shortcut the exponential search tree that DPLL must traverse in full. The learned clauses encode structural information about the ordering that tree-like reasoning cannot efficiently capture. DPLL is polynomially equivalent to tree-like resolution, and tree-like resolution has exponential lower bounds for these formulas. CDCL escapes this by operating in the richer proof system of general resolution. The practice was right: learning from contradictions is exponentially more powerful than pure branching.