An Exponential Separation between Deterministic CDCL and DPLL Solvers
This provides a theoretical separation for SAT solving, showing CDCL can exponentially outperform DPLL, which is foundational for automated reasoning and constraint satisfaction.
The authors proved that a deterministic CDCL SAT solver with a specific branching heuristic solves Ordering Principle formulas in polynomial time, while tree-like resolution requires exponential proof size, establishing an exponential separation between CDCL and DPLL solvers.
We prove that there exists a deterministic configuration of Conflict Driven Clause Learning (CDCL) SAT solvers using a variant of the VSIDS branching heuristic that solves instances of the Ordering Principle (OP) CNF formulas in time polynomial in n, where n is the number of variables in such formulas. Since tree-like resolution is known to have an exponential lower bound for proof size for OP formulas, it follows that CDCL under this configuration has an exponential separation with any solver that is polynomially equivalent to tree-like resolution and therefore any configuration of DPLL SAT solvers.