Hader, T., Irfan, A., & Graham-Lengrand, S. (2025, August 2). Decision Heuristics in MCSat [Presentation]. 10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025), Stuttgart, Germany.
E192-04 - Forschungsbereich Formal Methods in Systems Engineering E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies
-
Date (published):
2-Aug-2025
-
Event name:
10th International Workshop on Satisfiability Checking and Symbolic Computation (SC-Square 2025)
en
Event date:
2-Aug-2025
-
Event place:
Stuttgart, Germany
-
Keywords:
Decision heuristics; MCSat; SAT; SMT
en
Abstract:
The Model Constructing Satisfiability (MCSat) approach to Satisfiability Modulo Theories (SMT) has demonstrated strong performance when handling complex theories such as nonlinear arithmetic. Despite being in development for over a decade, there has been limited research on the heuristics utilized by MCSat solvers as in Yices2. In this paper, we discuss the decision heuristics employed in the MCSat approach of Yices2 and empirically show their significance on QF_NRA and QF_NIA benchmarks. Additionally, we propose new ideas to enhance these heuristics by leveraging theory-specific reasoning and drawing inspiration from recent advancements in SAT solvers. Our new version of the MCSat Yices2 solver not only solves more nonlinear arithmetic benchmarks than before but is also more efficient compared to other leading SMT solvers.