{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T00:30:23Z","timestamp":1760056223530,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986819"},{"type":"electronic","value":"9783031986826"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_3","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:13:39Z","timestamp":1753154019000},"page":"42-56","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Decision Heuristics in\u00a0MCSat"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Hader","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7791-9021","authenticated-orcid":false,"given":"Ahmed","family":"Irfan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2112-7284","authenticated-orcid":false,"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2020.100633","volume":"119","author":"E \u00c1brah\u00e1m","year":"2021","unstructured":"\u00c1brah\u00e1m, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Log. Algebraic Methods Program. 119, 100633 (2021)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A Versatile and Industrial-Strength SMT Solver. Presented at the (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"3_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 1267\u20131329. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201017","DOI":"10.3233\/FAIA201017"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: International Conference on Computer Aided Verification, pp. 133\u2013152. Springer (2024)","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"3_CR6","unstructured":"Biere, A., Fleury, M.: Chasing target phases. In: Workshop on the Pragmatics of SAT (2020)"},{"key":"3_CR7","unstructured":"Biere, A., Fleury, M., Froleyks, N., Heule, M.J.: The SAT museum. In: POS@ SAT, pp. 72\u201387 (2023)"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Biere, A., Fr\u00f6hlich, A.: Evaluating CDCL variable scoring schemes. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 405\u2013422. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_29","DOI":"10.1007\/978-3-319-24318-4_29"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.S., Nachmanson, L.: Arithmetic solving in Z3. In: CAV (1). Lecture Notes in Computer Science, vol. 14681, pp. 26\u201341. Springer (2024)","DOI":"10.1007\/978-3-031-65627-9_2"},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"1515","DOI":"10.1613\/jair.1.13666","volume":"74","author":"S Cai","year":"2022","unstructured":"Cai, S., Zhang, X., Fleury, M., Biere, A.: Better decision heuristics in cdcl through local search and target phases. J. Artif. Intell. Res. 74, 1515\u20131563 (2022)","journal-title":"J. Artif. Intell. Res."},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-319-94144-8_23","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Cimatti","year":"2018","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 383\u2013398. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_23"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log. 19(3), 19:1\u201319:52 (2018)","DOI":"10.1145\/3230639"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360\u2013368. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 737\u2013744. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"3_CR16","unstructured":"Dutertre, B.: An empirical evaluation of SAT solvers on bit-vector problems. In: SMT. CEUR Workshop Proceedings, vol.\u00a02854, pp. 15\u201325. CEUR-WS.org (2020)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 502\u2013518. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"989","DOI":"10.1613\/JAIR.1.16163","volume":"81","author":"K Fazekas","year":"2024","unstructured":"Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., Biere, A.: Satisfiability modulo user propagators. J. Artif. Intell. Res. 81, 989\u20131017 (2024). https:\/\/doi.org\/10.1613\/JAIR.1.16163","journal-title":"J. Artif. Intell. Res."},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Graham-Lengrand, S., Jovanovic, D., Dutertre, B.: Solving bitvectors with MCSAT: explanations from bits and pieces. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Intl. Joint Conf. on Automated Reasoning (IJCAR), Part I. LNCS, vol. 12166, pp. 103\u2013121. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_7","DOI":"10.1007\/978-3-030-51074-9_7"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Hader, T., Kaufmann, D., Irfan, A., Graham-Lengrand, S., Kov\u00e1cs, L.: MCSat-based finite field reasoning in the yices2 SMT solver (short paper). In: IJCAR (1). Lecture Notes in Computer Science, vol. 14739, pp. 386\u2013395. Springer (2024)","DOI":"10.1007\/978-3-031-63498-7_23"},{"key":"3_CR21","unstructured":"Irfan, A., Graham-Lengrand, S.: Arrays reasoning in MCSat. In: SMT@CAV. CEUR Workshop Proceedings, vol.\u00a03725, pp. 24\u201335. CEUR-WS.org (2024)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-52234-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Jovanovi\u0107","year":"2017","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 330\u2013346. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_18"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Jovanovic, D., Barrett, C., de\u00a0Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Intl. Conf on Formal Methods in Computer-Aided Design (FMCAD), pp. 173\u2013180. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.7027033","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-319-40970-2_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"JH Liang","year":"2016","unstructured":"Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for SAT solvers. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 123\u2013140. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_9"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"3_CR26","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Jovanovic, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Intl. Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol.\u00a07737, pp. 1\u201312. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"9","key":"3_CR28","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"LM de Moura","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"3_CR29","unstructured":"Nalbach, J., Kremer, G., \u00c1brah\u00e1m, E.: On variable orderings in MCSAT for non-linear real arithmetic. In: SC-square@ SIAM AG (2019)"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Abstract DPLL and abstract DPLL modulo theories. In: Baader, F., Voronkov, A. (eds.) Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol.\u00a03452, pp. 36\u201350. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-32275-7_3","DOI":"10.1007\/978-3-540-32275-7_3"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-72788-0_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"K Pipatsrisawat","year":"2007","unstructured":"Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 294\u2013299. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_28"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Preiner, M., Schurr, H.J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2024 (non-incremental benchmarks), April 2024. https:\/\/doi.org\/10.5281\/zenodo.11061097","DOI":"10.5281\/zenodo.11061097"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-66167-4_2","volume-title":"Frontiers of Combining Systems","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Tinelli, C., Jovanovi\u0107, D., Barrett, C.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 22\u201340. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_2"},{"key":"3_CR34","unstructured":"Ryan, L.: Efficient algorithms for clause-learning SAT solvers (2004)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:39:15Z","timestamp":1759999155000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}