Document Open Access Logo

Generalizing CDCL with Graph Backtracking

Authors Robin Coutelier , Thomas Hader , Laura Kovács

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.14.pdf
  • Filesize: 0.96 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Automated reasoning
Keywords
  • SAT Solving
  • Backtracking
  • Conflict Analysis
  • CDCL

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.SAT.2026.14

Author Details

Robin Coutelier
  • TU Wien, Austria
Thomas Hader
  • TU Wien, Austria
Laura Kovács
  • TU Wien, Austria

Funding

The authors acknowledge support from the ERC Consolidator Grant ARTIST 101002685; the TU Wien Doctoral Colleges TrustACPS and SecInt; the FWF SpyCoDe SFB projects F8504; and the WWTF Grant ForSmart 10.47379/ICT22007.

Acknowledgements

We would like to thank Mathias Fleury, Michael Rawson, Clemens Eisenhofer, Márton Hajdu, and Pascal Fontaine for fruitful discussions. We also thank the anonymous reviewers for their feedback.

References

  1. Bruno Andreotti and Haniel Barbosa. Producing shorter congruence closure proofs in a state-of-the-art SMT solver. In VMCAI, volume 16417 of Lecture Notes in Computer Science, pages 1-20. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-15700-3_1.
  2. Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, and Andrei Voronkov. The vampire diary. In CAV (3), volume 15933 of Lecture Notes in Computer Science, pages 57-71. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_4.
  3. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical 2.0. In CAV (1), volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  4. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  5. Nikolaj S. Bjørner, Clemens Eisenhofer, and Laura Kovács. Satisfiability modulo custom theories in Z3. In VMCAI, volume 13881 of Lecture Notes in Computer Science, pages 91-105. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-24950-1_5.
  6. Shaowei Cai and Kaile Su. Configuration checking with aspiration in local search for SAT. In AAAI, pages 434-440. AAAI Press, 2012. URL: https://doi.org/10.1609/AAAI.V26I1.8133.
  7. Robin Coutelier, Mathias Fleury, and Laura Kovács. Lazy reimplication in chronological backtracking. In SAT, volume 305 of LIPIcs, pages 9:1-9:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.9.
  8. Robin Coutelier, Thomas Hader, and Laura Kovács. Generalizing CDCL with Graph Backtracking, 2026. URL: https://doi.org/10.48550/arXiv.2605.28220.
  9. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In SAT, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  10. Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. Satisfiability modulo user propagators. J. Artif. Intell. Res., 81:989-1017, 2024. URL: https://doi.org/10.1613/JAIR.1.16163.
  11. Matthew L. Ginsberg. Dynamic backtracking. J. Artif. Intell. Res., 1:25-46, 1993. URL: https://doi.org/10.1613/JAIR.1.
  12. Massimo Lauria, Jan Elffers, Jakob Nordström, and Marc Vinyals. Cnfgen: A generator of crafted benchmarks. In SAT, volume 10491 of Lecture Notes in Computer Science, pages 464-473. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_30.
  13. Sibylle Möhle and Armin Biere. Backing backtracking. In SAT, volume 11628 of Lecture Notes in Computer Science, pages 250-266. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_18.
  14. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In DAC, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  15. Alexander Nadel. Introducing Intel(R) SAT solver. In SAT, volume 236 of LIPIcs, pages 8:1-8:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.8.
  16. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In SAT, volume 10929 of Lecture Notes in Computer Science, pages 111-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_7.
  17. Coutelier Robin. NapSAT solver. Accessed March 2026. URL: https://github.com/RobCoutel/NapSAT.
  18. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  19. Mate Soos and Kuldeep S. Meel. Engineering an efficient probabilistic exact model counter. In CAV (3), volume 15933 of Lecture Notes in Computer Science, pages 72-91. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-98682-6_5.
  20. Niklas Sörensson and Armin Biere. Minimizing learned clauses. In SAT, volume 5584 of Lecture Notes in Computer Science, pages 237-243. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_23.
  21. Niklas Sörensson and Niklas Eén. Minisat 2.1 and minisat++ 1.0-sat race 2008 editions. SAT, page 31, 2009. Google Scholar
  22. Giuseppe Spallitta, Roberto Sebastiani, and Armin Biere. Disjoint projected enumeration for SAT and SMT without blocking clauses. Artif. Intell., 345:104346, 2025. URL: https://doi.org/10.1016/J.ARTINT.2025.104346.
  23. Andrei Voronkov. AVATAR: the architecture for first-order theorem provers. In CAV, volume 8559 of Lecture Notes in Computer Science, pages 696-710. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_46.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact