An Exponential Separation between Deterministic CDCL and DPLL Solvers

Sahil Samar, Marc Vinyals, Vijay Ganesh

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 instance…