Record link: 
http://hdl.handle.net/20.500.12708/232014
-
Title: 
Decision Heuristics in MCSat
en
Citation: 
Hader, T., Irfan, A., & Graham-Lengrand, S. (2025). Decision Heuristics in MCSat. In R. Piskac & Z. Rakamarić (Eds.), Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III (pp. 42–56). Springer. https://doi.org/10.1007/978-3-031-98682-6_3
-
Publisher DOI: 
10.1007/978-3-031-98682-6_3
-
Publication Type: 
Inproceedings - Full-Paper Contribution
en
Language: 
English
-
Authors: 
Hader, Thomas 
Irfan, Ahmed 
Graham-Lengrand, Stéphane 
-
Organisational Unit: 
E192-04 - Forschungsbereich Formal Methods in Systems Engineering 
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies 
-
Published in: 
Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III 
-
ISBN: 
978-3-031-98682-6
-
Volume: 
15933
-
DOI of the book: 
10.1007/978-3-031-98682-6
-
Date (published): 
23-Jul-2025
-
Event name: 
37th International Conference Computer Aided Verification (CAV 2025) 
en
Event date: 
23-Jul-2025 - 25-Jul-2025
-
Event place: 
Zagreb, Croatia
-
Number of Pages: 
15
-
Publisher: 
Springer, Cham
-
Peer reviewed: 
Yes
-
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.
en
Project title: 
Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 (European Commission) 
-
Research Areas: 
Logic and Computation: 100%
-
Science Branch: 
1020 - Informatik: 80%
1010 - Mathematik: 20%
-
Appears in Collections:
Conference Paper

Show full item record

Google ScholarTM

Check