MaxSMT solver with portfolio mode support
https://doi.org/10.15514/ISPRAS-2025-37(4)-10
Abstract
The MaxSMT problem is to determine the satisfiability of a first-order theory formula with constraints. The paper presents an approach to solving this problem for the case of quantifier-free theories, which are usually decidable and widely applicable in practice for software test generation. The approach includes a modified MaxSAT algorithm PrimalDualMaxRes, in which the use of a SAT solver is replaced by an SMT solver, as well as the implementation of the portfolio mode. The latter means that the final MaxSMT algorithm is run in parallel with several MaxSMT solvers, and the best one is taken as the result. Z3, Yices and Bitwuzla were chosen as the SMT solvers on which the portfolio mode is built. The approach is implemented using the open-source Kotlin library KSMT, which implements the infrastructure for working with a set of MaxSMT solvers. The paper also presents the first benchmark for the MaxSMT problem. The evaluation demonstrates the competitiveness of the proposed solution. The developed portfolio of MaxSMT solvers outperforms the existing MaxSMT solver νZ (Z3 project), solving instances from the benchmark more than four times faster.
About the Authors
Viktoriia Viktorovna FOMINA
Saint-Petersburg State University
Russian Federation
Russian Federation
Postgraduate student of the Faculty of Mathematics and Mechanics, St. Petersburg State University. Her research interests include program analysis.
Valentyn SOBOL
ITMO University
Russian Federation
Russian Federation
Lecturer at ITMO University and a graduate of Peter the Great St. Petersburg Polytechnic University. His scientific interests include static analysis of programs and symbolic execution.
Dmitry Vladimirovich KOZNOV
Saint-Petersburg State University
Russian Federation
Russian Federation
Dr. Sci. (Tech.), Associate Professor, Professor St. Petersburg State University (SPbSU). Research interests: software engineering, model-driven software development, program data, machine learning.
References
1. Alouneh, S., Abed, S. E., Al Shayeji, M. H., Mesleh, R. A comprehensive study and analysis on SAT-solvers: advances, usages and achievements. Artificial Intelligence Review, vol. 52, 2019, pp. 2575–2601.
2. Misonizhnik, A., Mordvinov, D. On Satisfiability of Nominal Subtyping with Variance // Proceedings of 33rd European Conference on Object-Oriented Programming (ECOOP 2019), 2019.
3. Barrett, C., Sebastiani, R., Seshia, S. A., Tinelli, C. Satisfiability modulo theories // Handbook of satisfiability. IOS Press, 2021, pp. 1267–1329.
4. Костюков, Ю. О., Батоев, К. А., Мордвинов, Д. А., Костицын, М. П., Мисонижник, А. В. Автоматическое доказательство корректности программ с динамической памятью. Труды ИСП РАН, том 31, вып. 5, 2019 г., стр. 37–62.
5. Barrett, C., Tinelli, C., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y. Satisfiability Modulo Theories: A Beginner’s Tutorial. International Symposium on Formal Methods, 2024, pp. 571– 596.
6. De Moura, L., Bjørner, N. Z3: An efficient SMT solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, 2008, March, pp. 337–340.
7. Dutertre, B. Yices 2.2. In International Conference on Computer Aided Verification, 2014, pp. 737–744.
8. Niemetz, A., Preiner, M. Bitwuzla. In International Conference on Computer Aided Verification, 2023, pp. 3–17.
9. Pasareanu, C. S., Phan, Q. S., Malacaria, P. Multi-run side-channel analysis using Symbolic Execution and Max-SMT // Proceedings of IEEE 29th Computer Security Foundations Symposium (CSF). 2016, pp. 387–400.
10. Brockschmidt, M., Larra, D., Oliveras, A., Rodrıguez-Carbonell, E., Rubio, A. Compositional safety verification with Max-SMT // Formal Methods in Computer-Aided Design (FMCAD). 2015, pp. 33–40.
11. Terra-Neves, M., Machado, N., Lynce, I., Manquinho, V. Concurrency debugging with MaxSMT // Proceedings of the AAAI Conference on Artificial Intelligence, vol. 33, No. 01, 2019, pp. 1608–1616.
12. Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A. Proving non-termination using Max-SMT // Proceedings of Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26. Springer, 2014, pp. 779–796.
13. Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A. Proving termination of imperative programs using Max-SMT. In 2013 Formal Methods in Computer-Aided Design, 2013, pp. 218–225.
14. Albert, E., Gordillo, P., Rubio, A., Schett, M. A. Synthesis of super-optimized smart contracts using max-smt. In International conference on computer aided verification, 2020, pp. 177–200.
15. Li, C. M., Manya, F. MaxSAT, hard and soft constraints. In Handbook of satisfiability. IOS Press, 2021, pp. 903–927.
16. Мисонижник А.В., Бабушкин А.А., Морозов С.А., Костюков Ю.О., Мордвинов Д.А., Кознов Д.В. Автоматическое тестирование LLVM-программ со сложными входными структурами данных. Труды ИСП РАН, том 34, вып. 4, 2022 г., стр. 49–62.
17. Chen, T., Zhang, X. S., Guo, S. Z., Li, H. Y., Wu, Y. State of the art: Dynamic symbolic execution for automated test generation. Future Generation Computer Systems, vol. 29(7), 2013, pp. 1758–1773.
18. Bjorner, N., Narodytska, N. Maximum satisfiability using cores and correction sets // Proceedings of Twenty-Fourth International Joint Conference on Artificial Intelligence, 2015, pp. 246–252.
19. Narodytska, N., Bacchus, F. Maximum satisfiability using core-guided MaxSAT resolution // Proceedings of the AAAI Conference on Artificial Intelligence, vol. 28, No. 1, 2014.
20. Morgado, A., Dodaro, C., Marques-Silva, J. Core-Guided MaxSAT with Soft Cardinality Constraints. Principles and Practice of Constraint Programming, 2014, pp. 564–573.
21. Bjørner, N., Phan, A. D., Fleckenstein, L. νz-an optimizing SMT solver // Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21, 2015, pp. 194–199.
22. KSMT, https://github.com/UnitTestBot/ksmt (дата обращения: 01.02.2025).
23. MaxSMT benchmark, https://github.com/viktoriia-fomina/ksmt/releases/tag/0.0.0 (дата обращения: 01.02.2025).
24. SMT-COMP 2023, https://smt-comp.github.io/2023/ (дата обращения: 01.02.2025).
25. GitHub hosted runners, https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners/about-github-hosted-runners (дата обращения: 01.02.2025).
26. Тестовый набор данных для задачи SMT, https://smt-lib.org/benchmarks.shtml (дата обращения: 01.02.2025).
27. Guthmann, O., Strichman, O., Trostanetski, A. Minimal unsatisfiable core extraction for SMT. In 2016 Formal Methods in Computer-Aided Design (FMCAD), 2016, pp. 57–64.
28. Haedicke, F., Frehse, S., Fey, G., Große, D., Drechsler, R. metaSMT: Focus on Your Application not on Solver Integration. 2011, p. 47.
29. Baier, D., Beyer, D., Friedberger, K. JavaSMT 3: Interacting with SMT solvers in Java // Proceedings of International Conference on Computer Aided Verification, 2021, pp. 195-208. DOI: 10.1007/978-3-030-81688-9_9.
30. Gario, M., Micheli, A. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms // Proceedings of SMT workshop, 2015.
31. Sebastiani, R., Trentin, P. OptiMathSAT: A tool for optimization modulo theories. Journal of Automated Reasoning, 64(3), 2020, pp. 423–460.
32. Cimatti, A., Griggio, A., Schaafsma, B. J., Sebastiani, R. The mathsat5 smt solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2013, pp. 93–107.
33. Sebastiani, R., Trentin, P. On optimization modulo theories, MaxSMT and sorting networks // Proceedings of International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2017, pp. 231–248.
34. Terekhov A.N., Romanovskii K.Y., Koznov D.V., Dolgov P.S., Ivanov A.N. RTST++: Methodology and a CASE tool for the development of information systems and software for real-time systems. Programming and Computer Software, 1999, 25 (5), pp. 276–281.
35. Кознов Д.В., Перегудов А.Ф., Бугайченко Д.Ю., Чернятчик Р.И., Казакова А.С., Павлинов А.А. Визуальная среда проектирования систем телевизионного вещания. Системное программирование, 2006, 2(1), стр. 142–168.
Review
For citations:
FOMINA V.V., SOBOL V., KOZNOV D.V. MaxSMT solver with portfolio mode support. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2025;37(4):177-188. (In Russ.) https://doi.org/10.15514/ISPRAS-2025-37(4)-10
Email this article 