Document Open Access Logo

Lazy Reimplication in Chronological Backtracking

Authors Robin Coutelier , Mathias Fleury , Laura Kovács

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.9.pdf
  • Filesize: 0.92 MB
  • 19 pages

Document Identifiers

Author Details

Robin Coutelier
  • TU Wien, Austria
Mathias Fleury
  • University Freiburg, Germany
Laura Kovács
  • TU Wien, Austria

Funding

The authors acknowledge support from the ERC Consolidator Grant ARTIST 101002685; the TU Wien Doctoral College TrustACPS; the FWF SpyCoDe SFB projects F8504; the WWTF Grant ForSmart 10.47379/ICT22007; the and the Amazon Research Award 2023 QuAT; the bwHPC of the state of Baden-Württemberg; the German Research Foundation (DFG) through grant INST 35/1597-1 FUGG; and a gift from Intel Corporation.

Acknowledgements

The first author’s Master thesis [Coutelier and others, 2023] conducted at the University of Liège under the supervision of Pascal Fontaine laid the foundations of this work. We thank him for his insights.

Cite AsGet BibTex

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

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Automated reasoning
Keywords
  • Chronological Backtracking
  • CDCL
  • Invariants
  • Watcher Lists

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. Predicting Learnt Clauses Quality in Modern SAT Solvers. In IJCAI, pages 399-404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf.
  2. Gilles Audemard and Laurent Simon. On the Glucose SAT solver. Int. J. Artif. Intell. Tools, 27(1):1840001:1-1840001:25, 2018. URL: https://doi.org/10.1142/S0218213018400018.
  3. Armin Biere. Adaptive Restart Strategies for Conflict Driven SAT Solvers. In SAT, volume 4996 of LNCS, pages 28-33. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_4.
  4. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel und Vijay Ganesh, editor, Computer Aided Verification - 36th International Conference, CAV 2024, Paris, France, July 24-27, 2024, LNCS. Springer, 2024. To appear. Google Scholar
  5. Armin Biere, Mathias Fleury, and Florian Pollitt. CaDiCaL_vivinst, IsaSAT, Gimsatul, Kissat, and TabularaSAT entering the SAT competition 2023. In SAT Competition 2023 - Solver and Benchmark Descriptions, volume B-2023-1 of Department of Computer Science Report Series B, pages 14-15. University of Helsinki, 2023. Google Scholar
  6. 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.
  7. Armin Biere, Matti Järvisalo, and Bejamin Kiesl. Preprocessing in SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 391-435. IOS Press, 2nd edition edition, 2021. Google Scholar
  8. Nikolaj S. Bjørner, Clemens Eisenhofer, and Laura Kovács. User-propagators for custom theories in SMT solving. In David Déharbe and Antti E. J. Hyvärinen, editors, Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022, volume 3185 of CEUR Workshop Proceedings, pages 71-79. CEUR-WS.org, 2022. URL: https://ceur-ws.org/Vol-3185/extended6630.pdf.
  9. Geoffrey Chu, Aaron Harwood, and Peter J. Stuckey. Cache Conscious Data Structures for Boolean Satisfiability Solvers. JSAT, 6(1-3):99-120, 2009. URL: https://satassociation.org/jsat/index.php/jsat/article/view/71.
  10. Robin Coutelier. RobCoutel/NapSAT. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:1308f5717399bd09dcad2de805cc42eaa5504854;origin=https://github.com/RobCoutel/NapSAT;visit=swh:1:snp:aff7ae6a3ea2f154e8a57a795ff68bea81d9baaa;anchor=swh:1:rev:df5a9ca4c2ddb6196dca5b89050634ce72d5fec3 (visited on 2024-08-05). URL: https://github.com/RobCoutel/NapSAT.
  11. Robin Coutelier et al. Chronological vs. Non-Chronological Backtracking in Satisfiability Modulo Theories. Master’s thesis, Université de Liège, Liège, Belgique, 2023. Google Scholar
  12. Mathias Fleury. arminbiere/cadical. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:eaf1bada31f3142996582c25a7df2118e7cacc98;origin=https://github.com/arminbiere/cadical;visit=swh:1:snp:53dfb8828f1ebfecc0e02187545b6762c277b5c9;anchor=swh:1:rev:5ce2e0a5a676d5682622005d56a50e5266f3e29b (visited on 2024-08-05). URL: https://github.com/arminbiere/cadical/tree/strong-backtrack.
  13. Mathias Fleury. m-fleury/glucose. Software, swhId: https://archive.softwareheritage.org/swh:1:dir:fc5f0bd80c6a9e9412c5a3f3fcde96bf17a36147;origin=https://github.com/m-fleury/glucose;visit=swh:1:snp:a2f7255914669f8ebcc24ec1124ef1ae31bb16d0;anchor=swh:1:rev:8a5c7117fda44781c56bba2e9a9520fca5450509 (visited on 2024-08-05). URL: https://github.com/m-fleury/glucose.
  14. Robin Coutelier Pascal Fontaine. ModularIT solver. Accessed March 2024. URL: https://gitlab.uliege.be/smt-modules/.
  15. Randy Hickey and Fahiem Bacchus. Trail saving on backtrack. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 46-61. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_4.
  16. Holger H Hoos and Thomas Stützle. SATLIB: An Online Resource for Research on SAT. Sat, 2000:283-292, 2000. Google Scholar
  17. Norbert Manthey. Watch Sat and LTO for CaDiCaL. In SAT Competition 2023 - Solver and Benchmark Descriptions, volume B-2023-1 of Department of Computer Science Report Series B, pages 10-11. University of Helsinki, 2023. Google Scholar
  18. Sibylle Möhle and Armin Biere. Backing Backtracking. In SAT, volume 11628 of LNCS, pages 250-266. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_18.
  19. 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.
  20. 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.
  21. Alexander Nadel and Vadim Ryvchin. Chronological Backtracking. In SAT, volume 10929 of LNCS, pages 111-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_7.
  22. Florian Pollitt. Cadical 1.9.4. Accessed March 2024. URL: https://github.com/arminbiere/cadical/tree/reimply-branch.
  23. 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.
  24. Niklas Sörensson and Armin Biere. Minimizing Learned Clauses. In SAT, volume 5584 of LNCS, pages 237-243. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_23.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact