DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.30

An Exponential Separation Between Deterministic CDCL and DPLL Solvers

Authors: Sahil Samar, Marc Vinyals, and Vijay Ganesh

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

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.

Cite as

Sahil Samar, Marc Vinyals, and Vijay Ganesh. An Exponential Separation Between Deterministic CDCL and DPLL Solvers. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{samar_et_al:LIPIcs.SAT.2026.30,
  author =	{Samar, Sahil and Vinyals, Marc and Ganesh, Vijay},
  title =	{{An Exponential Separation Between Deterministic CDCL and DPLL Solvers}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.30},
  URN =		{urn:nbn:de:0030-drops-263369},
  doi =		{10.4230/LIPIcs.SAT.2026.30},
  annote =	{Keywords: SAT solvers, CDCL, Proof Systems, VSIDS}
}

Search Results

Documents authored by Samar, Sahil

An Exponential Separation Between Deterministic CDCL and DPLL Solvers

Abstract

Cite as

Thanks for your feedback!

Could not send message