An Exponential Separation between Deterministic CDCL and DPLL Solvers

TL;DR

This paper demonstrates that a specific deterministic CDCL SAT solver can solve certain formulas efficiently, showing an exponential separation from DPLL solvers, which are limited by tree-like resolution bounds.

Contribution

It establishes an exponential separation between deterministic CDCL and DPLL solvers on the Ordering Principle formulas, highlighting the power of CDCL with a specific heuristic.

Findings

Deterministic CDCL solves OP formulas in polynomial time.

Tree-like resolution has exponential lower bounds for OP formulas.

CDCL outperforms DPLL on the studied formulas.

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.