2026-07-25T21:29:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20531 2024-11-27T23:17:56Z ddc:004 open_access

Lazy Reimplication in Chronological Backtracking Coutelier, Robin Fleury, Mathias Kovács, Laura Chronological Backtracking CDCL Invariants Watcher Lists 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robin Coutelier and Mathias Fleury and Laura Kovács 2024 Is Part Of LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2024.9 urn:nbn:de:0030-drops-205313 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9 eng https://creativecommons.org/licenses/by/4.0/legalcode