Overview Statistic: PDF-Downloads (blue) and Frontdoor-Views (gray)

Prioritised Unit Propagation by Partitioning the Watch Lists

  • Conflict Driven Clause Learning (CDCL) SAT solvers spend most of their execution time iterating through clauses in unit propagation. Efficient implementations of unit propagation mostly rely on the two watched literals (TWL) scheme, a specialised data structure watching two literals per clause to prevent as many clause lookups as possible. In this paper, we present Priority Propagation (PriPro)—a minimally invasive method to adapt unit propagation in existing SAT solvers. With PriPro the traditional TWL scheme is partitioned to allow for rearranging the order in which clauses are examined. This is used to achieve a prioritisation of certain clauses. Using PriPro in combination with a dynamic heuristic to prioritise resolvents from recent conflicts, the effectiveness of unit propagation can be increased. In the state-of-the-art CDCL SAT solver CaDiCaL modified to use PriPro, we obtained a 5–10 % speedup on the SAT Competition 2021 benchmark set in a fair comparison with the unmodified CaDiCaL.

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics - number of accesses to the document
Metadaten
Author:Benjamin KaiserORCiD, Robert Clausecker, Michael Mavroskoufis
Document Type:In Proceedings
Parent Title (English):Proceedings of the 14th International Workshop on Pragmatics of SAT co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)
Volume:3545
First Page:14
Last Page:34
Publisher:CEUR Workshop Proceedings
Year of first publication:2023
URL:https://ceur-ws.org/Vol-3545/paper2.pdf
Licence (German):License LogoCreative Commons - CC BY - Namensnennung 4.0 International
Accept ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.