MaxSMT solver with portfolio mode support

V. V. Fomina^a, V. Sobol^b, D. V. Koznov<sup>a

a</sup> Saint Petersburg State University
^b ITMO University

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 vZ (Z3 project), solving instances from the benchmark more than four times faster.

Keywords: MaxSMT, MaxSMT solver, KSMT, SMT solver, portfolio

DOI: 10.15514/ISPRAS-2025-37(4)-10