<div class="csl-bib-body">
<div class="csl-entry">Hader, T., Irfan, A., & Graham-Lengrand, S. (2025). Decision Heuristics in MCSat. In R. Piskac & Z. Rakamarić (Eds.), <i>Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III</i> (pp. 42–56). Springer. https://doi.org/10.1007/978-3-031-98682-6_3</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/232014
-
dc.description.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
dc.description.sponsorship
European Commission
-
dc.language.iso
en
-
dc.relation.ispartofseries
Lecture Notes in Computer Science
-
dc.subject
Decision heuristics
en
dc.subject
MCSat
en
dc.subject
SAT
en
dc.subject
SMT
en
dc.title
Decision Heuristics in MCSat
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
SRI International, United States of America (the)
-
dc.contributor.affiliation
SRI International, United States of America (the)
-
dc.contributor.editoraffiliation
Yale University, United States of America (the)
-
dc.contributor.editoraffiliation
Amazon (United States), United States of America (the)
-
dc.relation.isbn
978-3-031-98682-6
-
dc.relation.doi
10.1007/978-3-031-98682-6
-
dc.relation.issn
0302-9743
-
dc.description.startpage
42
-
dc.description.endpage
56
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
1611-3349
-
tuw.booktitle
Computer Aided Verification : 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III
-
tuw.container.volume
15933
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Springer
-
tuw.relation.publisherplace
Cham
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publication.orgunit
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies
-
tuw.publisher.doi
10.1007/978-3-031-98682-6_3
-
dc.description.numberOfPages
15
-
tuw.author.orcid
0009-0002-8920-5469
-
tuw.author.orcid
0000-0001-7791-9021
-
tuw.author.orcid
0000-0002-2112-7284
-
tuw.editor.orcid
0000-0002-3267-0776
-
tuw.event.name
37th International Conference Computer Aided Verification (CAV 2025)
en
tuw.event.startdate
23-07-2025
-
tuw.event.enddate
25-07-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Zagreb
-
tuw.event.country
HR
-
tuw.event.presenter
Hader, Thomas
-
tuw.event.track
Multi Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.fulltext
no Fulltext
-
item.openairetype
conference paper
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.languageiso639-1
en
-
item.grantfulltext
none
-
crisitem.project.funder
European Commission
-
crisitem.project.grantno
ERC Consolidator Grant 2020
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
