Unit Propagation with Stable Watches (Short Paper)

Authors Markus Iser , Tomáš Balyo

Thumbnail PDF


  • Filesize: 0.85 MB
  • 8 pages

Document Identifiers

Author Details

Markus Iser
  • Karlsruhe Institute of Technology (KIT), Germany
Tomáš Balyo
  • CAS Software AG, Karlsruhe, Germany

Cite AsGet BibTex

Markus Iser and Tomáš Balyo. Unit Propagation with Stable Watches (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Unit Propagation
  • Two-Watched Literals
  • Literal Stability


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Tomáš Balyo, Nils Froleyks, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proceedings of SAT Competition 2020, pages 50-53. Department of Computer Science, University of Helsinki, 2020. Google Scholar
  2. Robert Brummayer and Armin Biere. Lemmas on demand for the extensional theory of arrays. J. Satisf. Boolean Model. Comput., 6(1-3):165-201, 2009. Google Scholar
  3. Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda. SAT Competition 2020. Artificial Intelligence, Accepted for Publication, 2021. Google Scholar
  4. Ian P. Gent. Optimal implementation of watched literals and more general techniques. J. Artif. Intell. Res., 48:231-251, 2013. Google Scholar
  5. Steffen Hölldobler, Norbert Manthey, and Ari Saptawijaya. Improving resource-unaware SAT solvers. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 519-534. Springer, 2010. Google Scholar
  6. Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Ann. Math. Artif. Intell., 1:167-187, 1990. Google Scholar
  7. Stepan Kochemazov. F2TRC: deterministic modifications of SC2018-SR2019 winners. In Tomáš Balyo, Nils Froleyks, Marijn J. H. Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, pages 21-22. Department of Computer Science, University of Helsinki, 2020. Google Scholar
  8. Joao P. Marques-Silva and Karem A. Sakallah. Grasp: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999. Google Scholar
  9. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535, 2001. Google Scholar
  10. Saeed Nejati, Jan Horácek, Catherine H. Gebotys, and Vijay Ganesh. Algebraic fault attack on SHA hash functions using programmatic SAT solvers. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 737-754, 2018. Google Scholar
  11. Dominik Schreiber, Damien Pellier, Humbert Fiorino, and Tomás Balyo. Efficient SAT encodings for hierarchical planning. In Ana Paula Rocha, Luc Steels, and H. Jaap van den Herik, editors, Proceedings of the 11th International Conference on Agents and Artificial Intelligence, ICAART 2019, Volume 2, Prague, Czech Republic, February 19-21, 2019, pages 531-538. SciTePress, 2019. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail