<div class="csl-bib-body">
<div class="csl-entry">Coutelier, R., Fleury, M., & Kovacs, L. (2024). Lazy Reimplication in Chronological Backtracking. In S. Chakraborty & J.-H. R. Jiang (Eds.), <i>27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)</i> (pp. 9:1-9:19). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.SAT.2024.9</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/210852
-
dc.description.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.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.description.sponsorship
Amazon Research Awards
-
dc.language.iso
en
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
Chronological Backtracking
en
dc.subject
CDCL
en
dc.subject
Invariants
en
dc.subject
Watcher Lists
en
dc.title
Lazy Reimplication in Chronological Backtracking
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.relation.publication
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
-
dc.contributor.affiliation
University of Freiburg, Germany
-
dc.contributor.editoraffiliation
Indian Institute of Technology Bombay, India
-
dc.contributor.editoraffiliation
National Taiwan University, Taiwan (Province of China)
