The QSMA algorithm for quantifiers in SMT

Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called 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 OptiQSMA is also described and shown to preserve both partial correctness and termination. OptiQSMA is implemented in the YicesQS solver. 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 (LRA - Linear Rational Arithmetic, LIA - Linear Integer Arithmetic, NRA - Nonlinear Real Arithmetic, and NIA - Nonlinear Integer Arithmetic) and in the theory of bitvectors (BV) is included.