{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T03:49:11Z","timestamp":1777434551891,"version":"3.51.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031384981","type":"print"},{"value":"9783031384998","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents and proves totally correct a new algorithm, called<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QSMA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>QSMA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{QSMA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>QSMA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>implemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LIA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>LIA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{NIA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>NIA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LRA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>LRA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>,<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{NRA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>NRA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{BV}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>BV<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>categories and ranked second for the \u201clargest contribution\u201d award (single queries). It was the only solver to solve all<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LRA}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>LRA<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>instances, where it was about two orders of magnitude faster than the second best solver (Z3).<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_5","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"78-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["QSMA: A New Algorithm for\u00a0Quantified Satisfiability Modulo Theory and\u00a0Assignment"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\u00e9phane","family":"Graham-Lengrand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Vauthier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84\u201399. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction (short paper). In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) Short Presentations at LPAR-20. EPiC Series in Computing, vol. 35, pp. 15\u201327. EasyChair (2015)","DOI":"10.29007\/vv21"},{"issue":"3","key":"5_CR4","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/s10817-018-09510-y","volume":"64","author":"MP Bonacina","year":"2020","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: transition system and completeness. J. Autom. Reason. 64(3), 579\u2013609 (2020). https:\/\/doi.org\/10.1007\/s10817-018-09510-y","journal-title":"J. Autom. Reason."},{"key":"5_CR5","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: CDSAT for nondisjoint theories with shared predicates: arrays with abstract length. In: Hyv\u00e4rinen, A., D\u00e9harbe, D. (eds.) Proceedings of the SMT-20. CEUR Proceedings, vol. 3185, pp. 18\u201337. CEUR WS-org (2022)"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-021-09606-y","volume":"66","author":"MP Bonacina","year":"2022","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs. J. Autom. Reason. 66(1), 43\u201391 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09606-y","journal-title":"J. Autom. Reason."},{"issue":"2","key":"5_CR7","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161\u2013189 (2011). https:\/\/doi.org\/10.1007\/s10817-010-9213-y","journal-title":"J. Autom. Reason."},{"key":"5_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation - Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L de Moura","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13"},{"key":"5_CR10","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"},{"issue":"3","key":"5_CR11","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"DL Detlefs","year":"2005","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM"},{"key":"5_CR12","unstructured":"Dutertre, B.: Solving exists\/forall problems with Yices. In: Proceedings of the SMT-13 (2015)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167\u2013182. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_12"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"5_CR15","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":"5_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-030-81688-9_13","volume-title":"Computer Aided Verification","author":"D Jovanovi\u0107","year":"2021","unstructured":"Jovanovi\u0107, D., Dutertre, B.: Interpolation and model checking for nonlinear arithmetic. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 266\u2013288. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_13"},{"issue":"3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Design 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Design"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223\u2013237. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19"},{"key":"5_CR20","unstructured":"Moskal, M.: Fx7 or in software, it is all about quantifiers. System Descriptions at SMT-COMP (2007). http:\/\/smtcomp.cs.uiowa.edu\/2007\/descriptions\/fx7.pdf"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-319-96142-2_16","volume-title":"Computer Aided Verification","author":"A Niemetz","year":"2018","unstructured":"Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C.: Solving quantified bit-vectors using invertibility conditions. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 236\u2013255. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_16"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., de Moura, L.: Finding conflicting instances of quantified formulas in SMT. In: Claessen, K., Kuncak, V. (eds.) Proceedings of the FMCAD 2014, pp. 195\u2013202. ACM and IEEE (2014). https:\/\/dl.acm.org\/doi\/10.5555\/2682923.2682957","DOI":"10.1109\/FMCAD.2014.6987613"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T10:35:12Z","timestamp":1730025312000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}