Document Open Access Logo

DynamicSAT: Dynamic Configuration Tuning for SAT Solving

Authors Zhengyuan Shi , Wentao Jiang , Xindi Zhang , Jin Luo , Yun Liang , Zhufei Chu , Qiang Xu

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CP.2025.34.pdf
  • Filesize: 1.27 MB
  • 23 pages
HTML5 Logo HTML (experimental)
LIPIcs.CP.2025.34.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
  • Mathematics of computing → Combinatorial optimization
Keywords
  • Boolean satisfiability problem
  • configuration tuning
  • multi-armed bandit

Metrics

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

Abstract

Boolean Satisfiability (SAT) problem serves as a foundation for solving numerous real-world challenges. As problem complexity increases, so does the demand for sophisticated SAT solvers, which incorporate a variety of heuristics tailored to optimize performance for specific problem instances. However, a major limitation persists: a configuration that performs well on one instance may lead to inefficiencies on others. While previous approaches to automatic algorithm configuration set parameters prior to runtime, they fail to adapt to the dynamic evolution of problem characteristics during the solving process. We introduce DynamicSAT, a novel SAT solver framework that dynamically tunes configuration parameters during solving process. By adjusting parameters on-the-fly, DynamicSAT adapts to changes arising from clause learning, elimination, and other transformations, thus improving efficiency and robustness across diverse SAT instances. We demonstrate that DynamicSAT achieves significant performance gains over the state-of-the-art solver on 2024 SAT Competition Benchmark.

Cite As Get BibTex

Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu. DynamicSAT: Dynamic Configuration Tuning for SAT Solving. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CP.2025.34

Author Details

Zhengyuan Shi
  • The Chinese University of Hong Kong, Hong Kong
  • National Center of Technology Innovation for EDA, Nanjing, China
Wentao Jiang
  • Ningbo University, China
  • National Center of Technology Innovation for EDA, Nanjing, China
Xindi Zhang
  • Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Science, Beijing, China
Jin Luo
  • Peking University, Beijing, China
  • National Center of Technology Innovation for EDA, Nanjing, China
Yun Liang
  • Peking University, Beijing, China
Zhufei Chu
  • Ningbo University, China
Qiang Xu
  • The Chinese University of Hong Kong, Hong Kong
  • National Center of Technology Innovation for EDA, Nanjing, China

Funding

This work was supported in part by the Hong Kong Research Grants Council (RGC) under Grant No. 14212422, 14202824, and C6003-24Y, in part by National Technology Innovation Center for EDA, China and in part by the NSFC under Grant No. 62274100, No. T2293700 and No. T2293701.

Supplementary Materials

References

  1. Rajeev Agrawal. Sample mean based index policies by o (log n) regret for the multi-armed bandit problem. Advances in applied probability, 27(4):1054-1078, 1995. Google Scholar
  2. Carlos Ansótegui, Meinolf Sellmann, and Kevin Tierney. A gender-based genetic algorithm for the automatic configuration of algorithms. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, pages 142-157, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-04244-7_14.
  3. Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern sat solvers. In Twenty-first international joint conference on artificial intelligence. Citeseer, 2009. 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. In Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors, Proc. of SAT Competition 2024 - Solver, Benchmark and Proof Checker Descriptions, volume B-2024-1 of Department of Computer Science Report Series B, pages 8-10. University of Helsinki, 2024. Google Scholar
  5. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009. Google Scholar
  6. Ronen I Brafman. A simplifier for propositional formulas with many binary clauses. IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cybernetics), 34(1):52-59, 2004. URL: https://doi.org/10.1109/TSMCB.2002.805807.
  7. Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Combining vsids and chb using restarts in sat. In 27th International Conference on Principles and Practice of Constraint Programming, 2021. Google Scholar
  8. Stephen A Cook. The complexity of theorem-proving procedures. In Logic, automata, and computational complexity: The works of Stephen A. Cook, pages 143-152. 2023. URL: https://doi.org/10.1145/3588287.3588297.
  9. Stefan Falkner, Marius Lindauer, and Frank Hutter. Spysmac: Automated configuration and performance analysis of sat solvers. In International Conference on Theory and Applications of Satisfiability Testing, pages 215-222. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_16.
  10. ABKFM Fleury and Maximilian Heisinger. Cadical, kissat, paracooba, plingeling and treengeling entering the sat competition 2020. SAT COMPETITION, 2020:50, 2020. Google Scholar
  11. Armin Biere Mathias Fleury. Gimsatul, isasat, kissat. SAT COMPETITION, 10, 2022. Google Scholar
  12. Carla P Gomes, Bart Selman, Henry Kautz, et al. Boosting combinatorial search through randomization. AAAI/IAAI, 98(1998):431-437, 1998. Google Scholar
  13. Marijn Heule, Matti Järvisalo, Florian Lonsing, Martina Seidl, and Armin Biere. Clause elimination for sat and qsat. Journal of Artificial Intelligence Research, 53:127-168, 2015. URL: https://doi.org/10.1613/JAIR.4694.
  14. Andrei Horbach. A boolean satisfiability approach to the resource-constrained project scheduling problem. Annals of Operations Research, 181:89-107, 2010. URL: https://doi.org/10.1007/S10479-010-0693-2.
  15. Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Sequential model-based optimization for general algorithm configuration. In Learning and Intelligent Optimization: 5th International Conference, LION 5, Rome, Italy, January 17-21, 2011. Selected Papers 5, pages 507-523. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-25566-3_40.
  16. Frank Hutter, Holger H. Hoos, and Kevin Leyton-Brown. Sequential model-based optimization for general algorithm configuration. In Carlos A. Coello Coello, editor, Learning and Intelligent Optimization, pages 507-523, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-25566-3_40.
  17. Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown, and Thomas Stützle. ParamILS: an automatic algorithm configuration framework. Journal of Artificial Intelligence Research, 36:267-306, October 2009. URL: https://doi.org/10.1613/JAIR.2861.
  18. Frank Hutter, Marius Lindauer, Adrian Balint, Sam Bayless, Holger Hoos, and Kevin Leyton-Brown. The configurable sat solver challenge (cssc). Artificial Intelligence, 243:1-25, 2017. URL: https://doi.org/10.1016/j.artint.2016.09.006.
  19. Markus Iser and Christoph Jabs. Global Benchmark Database. In Supratik Chakraborty and Jie-Hong Roland Jiang, editors, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), volume 305 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:10, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2024.18.
  20. Serdar Kadioglu, Yuri Malitsky, Meinolf Sellmann, and Kevin Tierney. Isac-instance-specific algorithm configuration. In ECAI 2010, pages 751-756. IOS Press, 2010. URL: https://doi.org/10.3233/978-1-60750-606-5-751.
  21. Michael N Katehakis and Arthur F Veinott Jr. The multi-armed bandit problem: decomposition and computation. Mathematics of Operations Research, 12(2):262-268, 1987. URL: https://doi.org/10.1287/MOOR.12.2.262.
  22. Henry Kautz and Bart Selman. Unifying sat-based and graph-based planning. In IJCAI, volume 99, pages 318-325, 1999. URL: http://ijcai.org/Proceedings/99-1/Papers/047.pdf.
  23. Chu-Min Li, Fan Xiao, Mao Luo, Felip Manyà, Zhipeng Lü, and Yu Li. Clause vivification by unit propagation in cdcl sat solvers. Artificial Intelligence, 279:103197, 2020. URL: https://doi.org/10.1016/J.ARTINT.2019.103197.
  24. Chunxiao Li, Charlie Liu, Jonathan Chung, Piyush Jha, Vijay Ganesh, et al. A reinforcement learning based reset policy for cdcl sat solvers. arXiv preprint arXiv:2404.03753, 2024. Google Scholar
  25. Jia Hui Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czarnecki. Understanding vsids branching heuristics in conflict-driven clause-learning sat solvers. In Hardware and Software: Verification and Testing: 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings 11, pages 225-241. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-26287-1_14.
  26. Hongduo Liu, Peng Xu, Yuan Pu, Lihao Yin, Hui-Ling Zhen, Mingxuan Yuan, Tsung-Yi Ho, and Bei Yu. Neuroselect: Learning to select clauses in sat solvers. In Proceedings of the 61st ACM/IEEE Design Automation Conference, pages 1-6, 2024. URL: https://doi.org/10.1145/3649329.3656250.
  27. Yuri Malitsky, Deepak Mehta, and Barry O'Sullivan. Evolving instance specific algorithm configuration. In Proceedings of the International Symposium on Combinatorial Search, volume 4, pages 133-140, 2013. URL: https://doi.org/10.1609/SOCS.V4I1.18296.
  28. Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning sat solvers. In Handbook of satisfiability, pages 133-182. ios Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  29. João P Marques-Silva and Karem A Sakallah. Boolean satisfiability in electronic design automation. In Proceedings of the 37th Annual Design Automation Conference, pages 675-680, 2000. URL: https://doi.org/10.1145/337292.337611.
  30. David A McAllester. Truth maintenance. In AAAI, volume 90, pages 1109-1116, 1990. URL: http://www.aaai.org/Library/AAAI/1990/aaai90-164.php.
  31. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver. In Proceedings of the 38th annual Design Automation Conference, pages 530-535, 2001. URL: https://doi.org/10.1145/378239.379017.
  32. Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In 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 21, pages 111-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94144-8_7.
  33. Chanseok Oh. Between sat and unsat: the fundamental difference in cdcl sat. In International Conference on Theory and Applications of Satisfiability Testing, pages 307-323. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_23.
  34. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning sat solvers as resolution engines. Artificial intelligence, 175(2):512-525, 2011. URL: https://doi.org/10.1016/J.ARTINT.2010.10.002.
  35. Hadar Shavit and Holger H Hoos. Revisiting satzilla features in 2024. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024), pages 27-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. Google Scholar
  36. Zhengyuan Shi, Min Li, Yi Liu, Sadaf Khan, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, and Qiang Xu. Satformer: Transformer-based unsat core learning. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 1-4. IEEE, 2023. URL: https://doi.org/10.1109/ICCAD57390.2023.10323731.
  37. Zhengyuan Shi, Hongyang Pan, Sadaf Khan, Min Li, Yi Liu, Junhua Huang, Hui-Ling Zhen, Mingxuan Yuan, Zhufei Chu, and Qiang Xu. Deepgate2: Functionality-aware circuit representation learning. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 1-9. IEEE, 2023. URL: https://doi.org/10.1109/ICCAD57390.2023.10323798.
  38. Niklas Sorensson and Niklas Een. Minisat v1. 13-a sat solver with conflict-clause minimization. SAT, 2005(53):1-2, 2005. Google Scholar
  39. Lin Xu, Frank Hutter, Holger H Hoos, and Kevin Leyton-Brown. Satzilla: portfolio-based algorithm selection for sat. Journal of artificial intelligence research, 32:565-606, 2008. URL: https://doi.org/10.1613/JAIR.2490.
  40. Lin Xu, Frank Hutter, Jonathan Shen, Holger H Hoos, and Kevin Leyton-Brown. Satzilla2012: Improved algorithm selection based on cost-sensitive classification models. Proceedings of SAT Challenge, pages 57-58, 2012. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact