Coutelier, R., Fleury, M., & Kovacs, L. (2024). Lazy Reimplication in Chronological Backtracking. In S. Chakraborty & J.-H. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) (pp. 9:1-9:19). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.SAT.2024.9
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.
en
Project title:
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design: F 8500 (FWF - Österr. Wissenschaftsfonds) Effective Formal Methods for Smart-Contract Certification: ICT22-007 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Amazon Research Award for conducting research on "Testing Dafny for Unsoundness and Brittleness Bugs": Christakis - Fall 2023 ARA (Amazon Research Awards)
CC BY 4.0
