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}\) (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}\) is also described and shown to preserve both partial correctness and termination. \(\textsf{OptiQSMA}\) is implemented in the YicesQS solver. \(\textsf{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}\) —Linear Rational Arithmetic, \(\textsf{LIA}\) —Linear Integer Arithmetic, \(\textsf{NRA}\) —Nonlinear Real Arithmetic, and \(\textsf{NIA}\) —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( \(\textsf{BV}\) ) is included.
