The QSMA Algorithm for Quantifiers in SMT
Maria Paola Bonacina, Stéphane Graham-Lengrand, Christophe Vauthier · Journal of Automated Reasoning · 2025
Abstract Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called $$\textsf{QSMA}$$ QSMA (Quantified Satisfiability Modulo Assignment), for the satisfiability of an arbitrary quantified formula modulo a complete theory and an initial assignment. The algorithm is proved partially correct and terminating, so that its total correctness is established. An optimized variant called $$\textsf{OptiQSMA}$$ OptiQSMA is also described and shown to preserve both partial correctness and termination. $$\textsf{OptiQSMA}$$ OptiQSMA is implemented in the YicesQS solver. $$\textsf{OptiQSMA}$$ OptiQSMA enabled YicesQS to achieve top of the line results, especially in linear rational arithmetic, in the 2022, 2023, and 2024 editions of the International Satisfiability Modulo Theories Competition (SMT-COMP). A report on these results in four fragments of arithmetic ( $$\textsf{LRA}$$ LRA —Linear Rational Arithmetic, $$\textsf{LIA}$$ LIA —Linear Integer Arithmetic, $$\textsf{NRA}$$ NRA —Nonlinear Real Arithmetic, and $$\textsf{NIA}$$ NIA —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( $$\textsf{BV}$$ BV ) is included.