KIT | KIT-Bibliothek | Impressum | Datenschutz

Unit propagation with stable watches

Iser, Markus; Balyo, Tomáš

Abstract:

Unit propagation is the hottest path in CDCL SAT solvers, therefore the related data-structures, algorithms and implementation details are well studied and highly optimized. State-of-the-art implementations are based on reduced occurrence tracking with two watched literals per clause and one blocking literal per watcher in order to further reduce the number of clause accesses. In this paper, we show that using runtime statistics for watched literal selection can improve the performance of state-of-the-art SAT solvers. We present a method for efficiently keeping track of spans during which literals are satisfied and using this statistic to improve watcher selection. An implementation of our method in the SAT solver CaDiCaL can solve more instances of the SAT Competition 2019 and 2020 benchmark sets and is specifically strong on satisfiable cryptographic instances.


Verlagsausgabe §
DOI: 10.5445/IR/1000139917
Veröffentlicht am 10.11.2021
Originalveröffentlichung
DOI: 10.4230/LIPIcs.CP.2021.6
Scopus
Zitationen: 1
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2021
Sprache Englisch
Identifikator ISBN: 978-3-9597721-1-2
ISSN: 1868-8969
KITopen-ID: 1000139917
Erschienen in 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Ed.: L. D. Michel
Veranstaltung 27th International Conference on Principles and Practice of Constraint Programming (2021), Online, 25.10.2021 – 29.10.2021
Verlag Schloss Dagstuhl - Leibniz-Zentrum für Informatik (LZI)
Seiten Art.-Nr.: 6
Serie Leibniz International Proceedings in Informatics (LIPIcs) ; 210
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page