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}
}

Artifact

Software

DOI: 10.4230/artifacts.22496

RobCoutel/NapSAT

Authors: Robin Coutelier

Abstract

Cite as

Robin Coutelier. RobCoutel/NapSAT (Software, NapSAT Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-22496,
   title = {{RobCoutel/NapSAT}}, 
   author = {Coutelier, Robin},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1308f5717399bd09dcad2de805cc42eaa5504854;origin=https://github.com/RobCoutel/NapSAT;visit=swh:1:snp:aff7ae6a3ea2f154e8a57a795ff68bea81d9baaa;anchor=swh:1:rev:df5a9ca4c2ddb6196dca5b89050634ce72d5fec3}{\texttt{swh:1:dir:1308f5717399bd09dcad2de805cc42eaa5504854}} (visited on 2024-11-28)},
   url = {https://github.com/RobCoutel/NapSAT},
   doi = {10.4230/artifacts.22496},
}

Document

DOI: 10.4230/LIPIcs.SAT.2024.9

Lazy Reimplication in Chronological Backtracking

Authors: Robin Coutelier, Mathias Fleury, and Laura Kovács

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract

Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.

Cite as

Robin Coutelier, Mathias Fleury, and Laura Kovács. Lazy Reimplication in Chronological Backtracking. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9,
  author =	{Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura},
  title =	{{Lazy Reimplication in Chronological Backtracking}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{9:1--9:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9},
  URN =		{urn:nbn:de:0030-drops-205313},
  doi =		{10.4230/LIPIcs.SAT.2024.9},
  annote =	{Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists}
}

Search Results

Documents authored by Coutelier, Robin

Generalizing CDCL with Graph Backtracking

Abstract

Cite as

RobCoutel/NapSAT

Abstract

Cite as

Lazy Reimplication in Chronological Backtracking

Abstract

Cite as

Thanks for your feedback!

Could not send message