{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:47Z","timestamp":1754161847042,"version":"3.41.2"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"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,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"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 the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by incrementally constructing a model by assigning concrete values to theory variables and performing theory-level reasoning to learn lemmas when conflicts arise. Therefore, the selection of values can significantly impact the search process and the solver\u2019s performance. In this work, we propose guiding the MCSat search by utilizing assignment values discovered through local search. First, we present a theory-agnostic framework to seamlessly integrate local search techniques within the MCSat framework. Then, we highlight how to use the framework to design a search procedure for (quantifier-free) Nonlinear Integer Arithmetic (<jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathcal {NIA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>NIA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>), utilizing accelerated hill-climbing and a new operation called <jats:italic>feasible-sets jumping<\/jats:italic>. We implement the proposed approach in the MCSat engine of the <jats:sc>Yices2<\/jats:sc> solver, and empirically evaluate its performance over the <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\mathcal {NIA}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>NIA<\/mml:mi>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> benchmarks of SMT-LIB.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_6","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:45Z","timestamp":1753789665000},"page":"95-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Boosting MCSat Modulo Nonlinear Integer Arithmetic via\u00a0Local Search"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-0428-4403","authenticated-orcid":false,"given":"Enrico","family":"Lipparini","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Hader","sequence":"additional","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,30]]},"reference":[{"key":"6_CR1","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer (2022)"},{"key":"6_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"6_CR3","doi-asserted-by":"crossref","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. Frontiers in Artificial Intelligence and Applications, 2nd edn., vol. 336, pp. 1267\u20131329. IOS Press (2021)","DOI":"10.3233\/FAIA201017"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Nachmanson, L.: Arithmetic solving in z3. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification, pp. 26\u201341. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65627-9_2"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Cai, S., Li, B., Zhang, X.: Local search for SMT on linear integer arithmetic. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 227\u2013248. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-13188-2_12"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Cai, S., Li, B., Zhang, X.: Local search for satisfiability modulo integer arithmetic theories. ACM Trans. Comput. Logic 24(4) (2023)","DOI":"10.1145\/3597495"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-030-80223-3_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2021","author":"S Cai","year":"2021","unstructured":"Cai, S., Zhang, X.: Deep cooperation of CDCL and local search for SAT. In: Li, C.-M., Many\u00e0, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 64\u201381. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-80223-3_6"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Cai, S., Zhang, X., Fleury, M., Biere, A.: Better decision heuristics in CDCL through local search and target phases. J. Artif. Int. Res., 74 (2022)","DOI":"10.1613\/jair.1.13666"},{"key":"6_CR9","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":"6_CR10","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. Logic 19(3) (2018)","DOI":"10.1145\/3230639"},{"key":"6_CR11","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":"6_CR12","doi-asserted-by":"crossref","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) Automata Theory and Formal Languages, pp. 134\u2013183. Springer, Heidelberg (1975)","DOI":"10.1007\/3-540-07407-4_17"},{"key":"6_CR13","doi-asserted-by":"crossref","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: SAT (2015)","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201908\/ETAPS\u201908, pp. 337\u2013340. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","DOI":"10.1145\/1995376.1995394"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer-Aided Verification (CAV\u20192014). Lecture Notes in Computer Science, vol. 8559, pp. 737\u2013744. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Biere, A., Wintersteiger, C., Hamadi, Y.: Stochastic local search for Satisfiability Modulo Theories. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 29, no. 1 (2015)","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-319-41540-6_11","volume-title":"Computer Aided Verification","author":"Z Fu","year":"2016","unstructured":"Fu, Z., Su, Z.: XSat: a fast floating-point satisfiability solver. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 187\u2013209. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_11"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-72788-0_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"C Fuhs","year":"2007","unstructured":"Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340\u2013354. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-72788-0_33"},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-030-51074-9_7","volume-title":"Automated Reasoning","author":"S Graham-Lengrand","year":"2020","unstructured":"Graham-Lengrand, S., Jovanovi\u0107, D., Dutertre, B.: Solving Bitvectors with MCSAT: explanations from bits and pieces. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 103\u2013121. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_7"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Griggio, A., Phan, Q.-S., Sebastiani, R., Tomasi, S.: Stochastic local search for SMT: combining theory solvers with WalkSAT. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Frontiers of Combining Systems, pp. 163\u2013178. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24364-6_12"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Hader, T., Irfan, A., Graham-Lengrand, S.: Decision heuristics in MCSat. In: Computer Aided Verification (2025, to appear)","DOI":"10.1007\/978-3-031-98682-6_3"},{"key":"6_CR24","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":"6_CR25","doi-asserted-by":"crossref","unstructured":"Hader, T., Kaufmann, D., Kov\u00e1cs, L.: SMT solving over finite field arithmetic. In: LPAR. EPiC Series in Computing, vol.\u00a094, pp. 238\u2013256. EasyChair (2023)","DOI":"10.29007\/4n6w"},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Hernando, L., Mendiburu, A., Lozano, J.: Hill-climbing algorithm: let\u2019s go for a walk before finding the optimum. pp. 1\u20137 (2018)","DOI":"10.1109\/CEC.2018.8477836"},{"key":"6_CR27","unstructured":"Irfan, A., Graham-Lengrand, S.: Arrays reasoning in MCSat. In: SMT@CAV. CEUR Workshop Proceedings, vol. 3725, pp. 24\u201335. CEUR-WS.org (2024)"},{"key":"6_CR28","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D.: Solving nonlinear integer arithmetic with MCSAT. In: Bouajjani, A., Monniaux, D. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 330\u2013346. Springer, Cham (2017)","DOI":"10.1007\/978-3-319-52234-0_18"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Jovanovic, D., Barrett, C., de\u00a0Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 173\u2013180. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.7027033"},{"issue":"3\/4","key":"6_CR30","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1145\/2429135.2429155","volume":"46","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. ACM Commun. Comput. Algebra 46(3\/4), 104\u2013105 (2013)","journal-title":"ACM Commun. Comput. Algebra"},{"key":"6_CR31","unstructured":"Kautz, H.A., Sabharwal, A., Selman, B.: Incomplete algorithms. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, 2nd edn., vol. 336, pp. 213\u2013232. IOS Press (2021)"},{"key":"6_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-319-45641-6_21","volume-title":"Computer Algebra in Scientific Computing","author":"G Kremer","year":"2016","unstructured":"Kremer, G., Corzilius, F., \u00c1brah\u00e1m, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) CASC 2016. LNCS, vol. 9890, pp. 315\u2013335. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45641-6_21"},{"issue":"1","key":"6_CR33","doi-asserted-by":"crossref","first-page":"5","DOI":"10.2478\/ausi-2018-0001","volume":"10","author":"G Kremer","year":"2018","unstructured":"Kremer, G., \u00c1brah\u00e1m, E.: Modular strategic SMT solving with SMT-RAT. Acta Universitatis Sapientiae, Informatica 10(1), 5\u201325 (2018)","journal-title":"Acta Universitatis Sapientiae, Informatica"},{"key":"6_CR34","unstructured":"Li, B., Cai, S.: Local search for SMT on linear and multi-linear real arithmetic. In: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp. 1\u201310 (2023)"},{"key":"6_CR35","doi-asserted-by":"crossref","unstructured":"Li, H., Xia, B., Zhao, T.: Local search for solving satisfiability of polynomial formulas. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 87\u2013109. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37703-7_5"},{"key":"6_CR36","unstructured":"Lipparini, E.: Satisfiability modulo Nonlinear Arithmetic and Transcendental Functions via Numerical and Topological methods. Ph.D. thesis (2024)"},{"key":"6_CR37","doi-asserted-by":"crossref","unstructured":"Lipparini, E., Cimatti, A., Griggio, A., Sebastiani, R.: Handling polynomial and transcendental functions in SMT via unconstrained optimisation and topological degree test. In: Bouajjani, A., Hol\u00edk, L., Wu, Z. (eds.) Automated Technology for Verification and Analysis, pp. 137\u2013153. Springer, Cham (2022)International Publishing","DOI":"10.1007\/978-3-031-19992-9_9"},{"key":"6_CR38","doi-asserted-by":"crossref","unstructured":"Lipparini, E., Ratschan, S.: Satisfiability of non-linear transcendental arithmetic as a certificate search problem. In: Rozier, K.Y., Chaudhuri, S. (eds.) NASA Formal Methods, pp. 472\u2013488. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-33170-1_29"},{"key":"6_CR39","doi-asserted-by":"crossref","unstructured":"Lipparini, E., Ratschan, S.: Satisfiability of non-linear transcendental arithmetic as a certificate search problem. J. Autom. Reason. 69(1) (2025)","DOI":"10.1007\/s10817-024-09716-3"},{"key":"6_CR40","volume-title":"Hilbert\u2019s Tenth Problem","author":"YV Matiyasevich","year":"1993","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s Tenth Problem. MIT Press, Cambridge (1993)"},{"issue":"3","key":"6_CR41","doi-asserted-by":"crossref","first-page":"608","DOI":"10.1007\/s10703-017-0295-6","volume":"51","author":"A Niemetz","year":"2017","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Propagation based local search for bit-precise reasoning. Formal Methods Syst. Des. 51(3), 608\u2013636 (2017)","journal-title":"Formal Methods Syst. Des."},{"issue":"6","key":"6_CR42","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"6_CR43","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":"6_CR44","unstructured":"Preiner, M., Schurr, H.-J., Barrett, C., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2024 (non-incremental benchmarks) (2024)"},{"key":"6_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/11814948_28","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"S Prestwich","year":"2006","unstructured":"Prestwich, S., Lynce, I.: Local search for unsatisfiability. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 283\u2013296. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_28"},{"key":"6_CR46","doi-asserted-by":"crossref","unstructured":"Wang, Z., Zhan, B., Li, B., Cai, S.: Efficient local search for nonlinear real arithmetic. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 326\u2013349. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-50524-9_15"},{"issue":"1","key":"6_CR47","first-page":"221","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"6_CR48","doi-asserted-by":"crossref","unstructured":"Zhang, X., Li, B., Cai, S.: Deep combination of CDCL(T) and local search for satisfiability modulo non-linear integer arithmetic theory. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering, ICSE \u201924, New York, NY, USA. Association for Computing Machinery (2024)","DOI":"10.1145\/3597503.3639105"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:51Z","timestamp":1753789671000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 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":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}