Document Open Access Logo

Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT

Authors Jinghu Liang , Sami Cherif , Chu-Min Li

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.39.pdf
  • Filesize: 1.83 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Satisfiablity
  • Branching
  • Restart
  • Multi-Armed Bandit

Metrics

Abstract

Multi-Armed Bandit (MAB) mechanisms have proven effective for adaptive heuristic switching in modern CDCL SAT solvers, with Kissat_MAB and its variants demonstrating strong performance in recent SAT Competitions. However, while strategies like the Luby series generate restarts with high duration variability, standard bandit models treat each restart as a homogeneous unit. This mismatch can bias credit assignment and lead to suboptimal exploration–exploitation trade-offs between short and long restarts. In this paper, we study MAB-based heuristic selection under variable-duration restart policies and propose a duration-aware modification to both bandit feedback and selection mechanisms. Our approach normalizes and conditions rewards on the restarts and adapts exploration and exploitation accordingly, thereby better aligning bandit updates with the solver’s restart dynamics.

Cite As Get BibTex

Jinghu Liang, Sami Cherif, and Chu-Min Li. Not All Restarts Are Equal: MAB-Learning at the Right Time Scale for SAT. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.39

Author Details

Jinghu Liang
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Sami Cherif
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France
Chu-Min Li
  • MIS UR 4290, Université de Picardie Jules Verne, Amiens, France

Funding

This work is supported by the project ANR-24-CE23-6126 (BforSAT), funded by the French National Research Agency (ANR), as well as the Chair ANR-19-CHIA-0013-01 (MASSAL’IA), co-funded by ANR and the electricity distribution network operator Enedis. It was granted access to HPC resources of "Plateforme MatriCS" within University of Picardie Jules Verne, co-funded by the European Union with the European Regional Development Fund (FEDER) and the Hauts-De-France Regional Council.

Supplementary Materials

References

  1. Gilles Audemard and Laurent Simon. Refining restarts strategies for SAT and UNSAT. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 118-126. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_11.
  2. Peter Auer, Nicolò Cesa-Bianchi, and Paul Fischer. Finite-time analysis of the multiarmed bandit problem. Mach. Learn., 47(2-3):235-256, 2002. URL: https://doi.org/10.1023/A:1013689704352.
  3. Armin Biere. Cadical at the sat race 2019. SAT RACE, 2019:8, 2019. Google Scholar
  4. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. Cadical, gimsatul, isasat and kissat entering the sat competition 2024. Proc. of SAT Competition, 8, 2024. Google Scholar
  5. Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximilian Heisinger. Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions, pages 50-53, 2020. Google Scholar
  6. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  7. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. On the refinement of conflict history search through multi-armed bandit. In 32nd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2020, Baltimore, MD, USA, November 9-11, 2020, pages 264-271. IEEE, 2020. URL: https://doi.org/10.1109/ICTAI50040.2020.00050.
  8. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Combining VSIDS and CHB using restarts in SAT. In Laurent D. Michel, editor, 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, pages 20:1-20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CP.2021.20.
  9. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Kissat mab: Combining vsids and chb through multi-armed bandit. Proceedings of SAT Competition 2021: Solver and Benchmark Descriptions, pages 50-53, 2021. Google Scholar
  10. Stephen A. Cook. The complexity of theorem-proving procedures. In Michael A. Harrison, Ranan B. Banerji, and Jeffrey D. Ullman, editors, Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, May 3-5, 1971, Shaker Heights, Ohio, USA, pages 151-158. ACM, 1971. URL: https://doi.org/10.1145/800157.805047.
  11. Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong, and Xinyun Wu. A self-optimizing framework for sat solvers via population evolution and large language model collaboration. In Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions, pages 15-17, 2025. Google Scholar
  12. Niklas Eén and Niklas Sörensson. An extensible sat-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  13. Jinbo Huang. The effect of restarts on the efficiency of clause learning. In Manuela M. Veloso, editor, IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, pages 2318-2323, 2007. URL: http://ijcai.org/Proceedings/07/Papers/373.pdf.
  14. Frédéric Koriche, Christophe Lecoutre, Anastasia Paparrizou, and Hugues Wattez. Best heuristic identification for constraint satisfaction. In IJCAI 2022, pages 1859-1865. ijcai.org, 2022. URL: https://doi.org/10.24963/IJCAI.2022/258.
  15. Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Boosting branch-and-bound maxsat solvers with clause learning. AI Commun., 35(2):131-151, 2022. URL: https://doi.org/10.3233/AIC-210178.
  16. Chunxiao Li, Noah Fleming, Marc Vinyals, Toniann Pitassi, and Vijay Ganesh. Towards a complexity-theoretic understanding of restarts in SAT solvers. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 233-249. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_17.
  17. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Exponential recency weighted average branching heuristic for SAT solvers. In Dale Schuurmans and Michael P. Wellman, editors, Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, February 12-17, 2016, Phoenix, Arizona, USA, pages 3434-3440. AAAI Press, 2016. URL: https://doi.org/10.1609/AAAI.V30I1.10439.
  18. Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 123-140. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_9.
  19. Jia Hui Liang, Hari Govind V. K., Pascal Poupart, Krzysztof Czarnecki, and Vijay Ganesh. An empirical study of branching heuristics through the lens of global learning rate. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10491 of Lecture Notes in Computer Science, pages 119-135. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66263-3_8.
  20. Jia Hui Liang, Chanseok Oh, Vijay Ganesh, Krzysztof Czarnecki, and Pascal Poupart. Maple-comsps lrb vsids and maplecomsps chb vsids. Proc. of SAT Competition, pages 20-21, 2017. Google Scholar
  21. Jia Hui Liang, Chanseok Oh, Minu Mathew, Ciza Thomas, Chunxiao Li, and Vijay Ganesh. Machine learning-based restart policy for CDCL SAT solvers. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing - SAT 2018 - 21st International Conference, SAT 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10929 of Lecture Notes in Computer Science, pages 94-110. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_6.
  22. Jinghu LIANG. DA_kissat_MAB. Software, (visited on 2026-05-18). URL: https://github.com/JinghuLiang/Duration_Aware_kissat_MAB
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.25917
  23. Jinjin Liu, Jianmin Zhang, and Yan Sun. Kissat mab-dc in sat competition 2024. Proceedings of SAT Competition 2024 : Solver, Benchmark and Proof Checker Descriptions, page 20, 2024. Google Scholar
  24. Michael Luby, Alistair Sinclair, and David Zuckerman. Optimal speedup of las vegas algorithms. In Second Israel Symposium on Theory of Computing Systems, ISTCS 1993, Natanya, Israel, June 7-9, 1993, Proceedings, pages 128-133. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/ISTCS.1993.253477.
  25. Mao Luo, Chu-Min Li, Fan Xiao, Felip Manya, and Zhipeng Lu. An effective learnt clause minimization approach for cdcl sat solvers. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI-17), pages 703-711, 2017. Google Scholar
  26. 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. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  27. Anastasia Paparrizou and Hugues Wattez. Perturbing branching heuristics in constraint solving. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, Lecture Notes in Computer Science, pages 496-513. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_29.
  28. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
  29. Hugues Wattez, Frédéric Koriche, Christophe Lecoutre, Anastasia Paparrizou, and Sébastien Tabary. Learning variable ordering heuristics with multi-armed bandits and restarts. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors, ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), Frontiers in Artificial Intelligence and Applications, pages 371-378. IOS Press, 2020. URL: https://doi.org/10.3233/FAIA200115.
  30. Wei Xia and Roland H. C. Yap. Learning robust search strategies using a bandit-based approach. In Sheila A. McIlraith and Kilian Q. Weinberger, editors, Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pages 6657-6665. AAAI Press, 2018. URL: https://doi.org/10.1609/AAAI.V32I1.12211.
  31. Zhihui Xie, Xu Liu, and Shuai Li. Multi-armed bandit algorithms for the boolean satisfiability problem: A survey. In Proceedings of the International Symposium on Combinatorial Search, volume 18, pages 221-229, 2025. Google Scholar
  32. Jiongzhi Zheng, Kun He, Zhuo Chen, Jianrong Zhou, and Chu-Min Li. Combining hybrid walking strategy with kissat mab, cadical, and lstech-maple. SAT COMPETITION, 2022:20, 2022. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact