An Exponential Separation between Deterministic CDCL and DPLL Solvers
Computational Complexity
2026-03-18 v1
Abstract
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.
Keywords
Cite
@article{arxiv.2603.16156,
title = {An Exponential Separation between Deterministic CDCL and DPLL Solvers},
author = {Sahil Samar and Marc Vinyals and Vijay Ganesh},
journal= {arXiv preprint arXiv:2603.16156},
year = {2026}
}