DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.14

Generalizing CDCL with Graph Backtracking

Authors: Robin Coutelier, Thomas Hader, and Laura Kovács

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

Abstract

We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound, complete, and terminating. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.

Cite as

Robin Coutelier, Thomas Hader, and Laura Kovács. Generalizing CDCL with Graph Backtracking. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{coutelier_et_al:LIPIcs.SAT.2026.14,
  author =	{Coutelier, Robin and Hader, Thomas and Kov\'{a}cs, Laura},
  title =	{{Generalizing CDCL with Graph Backtracking}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{14:1--14:18},
  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.14},
  URN =		{urn:nbn:de:0030-drops-263203},
  doi =		{10.4230/LIPIcs.SAT.2026.14},
  annote =	{Keywords: SAT Solving, Backtracking, Conflict Analysis, CDCL}
}

Search Results

Documents authored by Hader, Thomas

Generalizing CDCL with Graph Backtracking

Abstract

Cite as

Thanks for your feedback!

Could not send message