The QSMA Algorithm for Quantifiers in SMT

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}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>QSMA</mml:mi> </mml:math> ( 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}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>OptiQSMA</mml:mi> </mml:math> is also described and shown to preserve both partial correctness and termination. $$\textsf{OptiQSMA}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>OptiQSMA</mml:mi> </mml:math> is implemented in the YicesQS solver. $$\textsf{OptiQSMA}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>OptiQSMA</mml:mi> </mml:math> 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}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LRA</mml:mi> </mml:math> —Linear Rational Arithmetic, $$\textsf{LIA}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>LIA</mml:mi> </mml:math> —Linear Integer Arithmetic, $$\textsf{NRA}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>NRA</mml:mi> </mml:math> —Nonlinear Real Arithmetic, and $$\textsf{NIA}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>NIA</mml:mi> </mml:math> —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( $$\textsf{BV}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>BV</mml:mi> </mml:math> ) is included.