{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T16:00:08Z","timestamp":1758124808802,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656262"},{"type":"electronic","value":"9783031656279"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Satisfiability Modulo Theories on arithmetic theories have significant applications in many important domains. Previous efforts have been mainly devoted to improving the techniques and heuristics in sequential SMT solvers. With the development of computing resources, a promising direction to boost performance is parallel and even distributed SMT solving. We explore this potential in a divide-and-conquer view and propose a novel dynamic parallel framework with variable-level partitioning. To the best of our knowledge, this is the first attempt to perform variable-level partitioning for arithmetic theories. Moreover, we enhance the interval constraint propagation algorithm, coordinate it with Boolean propagation, and integrate it into our variable-level partitioning strategy. Our partitioning algorithm effectively capitalizes on propagation information, enabling efficient formula simplification and search space pruning. We apply our method to three state-of-the-art SMT solvers, namely CVC5, OpenSMT2, and Z3, resulting in efficient parallel SMT solvers. Experiments are carried out on benchmarks of linear and non-linear arithmetic over both real and integer variables, and our variable-level partitioning method shows substantial improvements over previous partitioning strategies and is particularly good at non-linear theories.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_4","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"68-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Distributed SMT Solving Based on\u00a0Dynamic Variable-Level Partitioning"],"prefix":"10.1007","author":[{"given":"Mengyu","family":"Zhao","sequence":"first","affiliation":[]},{"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[]},{"given":"Yuhang","family":"Qian","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"4_CR1","unstructured":"Asadzade, M., Blicha, M., Hyv\u00e4rinen, A., Otoni, R., Sharygina, N.: The opensmt solver in SMT-COMP 2022. In: 17th International Satisfiability Modulo Theories Competition (SMT-COMP 2022) (2022)"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Benhamou, F., Granvilliers, L.: Chapter 16 - continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol.\u00a02, pp. 571\u2013603. Elsevier (2006)","DOI":"10.1016\/S1574-6526(06)80020-9"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"790","DOI":"10.1007\/978-3-540-74970-7_56","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2007","author":"L Bordeaux","year":"2007","unstructured":"Bordeaux, L., Hamadi, Y., Vardi, M.Y.: An analysis of slow convergence in interval propagation. In: Bessi\u00e8re, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 790\u2013797. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74970-7_56"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: SMT-based verification of hybrid systems. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a026, pp. 2100\u20132105 (2012)","DOI":"10.1609\/aaai.v26i1.8442"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: 2011 33rd International Conference on Software Engineering (ICSE), pp. 331\u2013340 (2011)","DOI":"10.1145\/1985793.1985839"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-24318-4_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Corzilius","year":"2015","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"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_11"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Meyer, P.J.: An SMT-based approach to fair termination analysis. In: 2015 Formal Methods in Computer-Aided Design (FMCAD), pp. 49\u201356 (2015)","DOI":"10.1109\/FMCAD.2015.7542252"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Methods Syst. Des. 30, 179\u2013198 (2007)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR11","unstructured":"Franz\u00e9n, A., Cimatti, A., Nadel, A., Sebastiani, R., Shalev, J.: Applying SMT in symbolic execution of microcode. In: Formal Methods in Computer Aided Design, pp. 121\u2013128 (2010)"},{"key":"4_CR12","unstructured":"Gao, S., Ganai, M., Ivan\u010di\u0107, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In: Formal Methods in Computer Aided Design, pp. 81\u201389 (2010)"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"4_CR14","unstructured":"Herbort, S., Ratz, D.: Improving the efficiency of a nonlinear-system-solver using a componentwise newton method (1997)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-642-34188-5_8","volume-title":"Hardware and Software: Verification and Testing","author":"MJH Heule","year":"2012","unstructured":"Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A.: Cube and conquer: guiding CDCL SAT solvers by lookaheads. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 50\u201365. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34188-5_8"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-030-28423-7_6","volume-title":"Numerical Software Verification","author":"C Huang","year":"2019","unstructured":"Huang, C., Kong, S., Gao, S., Zufferey, D.: Evaluating branching heuristics in interval constraint propagation for satisfiability. In: Zamani, M., Zufferey, D. (eds.) NSV 2019. LNCS, vol. 11652, pp. 85\u2013100. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-28423-7_6"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/11814948_39","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"AEJ Hyv\u00e4rinen","year":"2006","unstructured":"Hyv\u00e4rinen, A.E.J., Junttila, T., Niemel\u00e4, I.: A distribution method for solving SAT in grids. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 430\u2013435. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814948_39"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-319-40970-2_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"AEJ Hyv\u00e4rinen","year":"2016","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 547\u2013553. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_35"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-319-24318-4_27","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"AEJ Hyv\u00e4rinen","year":"2015","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Sharygina, N.: Search-space partitioning for parallelizing SMT solvers. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 369\u2013386. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_27"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Hyv\u00e4rinen, A.E., Wintersteiger, C.M.: Parallel satisfiability modulo theories. In: Handbook of Parallel Constraint Reasoning, pp. 141\u2013178 (2018)","DOI":"10.1007\/978-3-319-63516-3_5"},{"key":"4_CR21","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Sharygina, N.: Lookahead in partitioning SMT. In: 2021 Formal Methods in Computer Aided Design (FMCAD), pp. 271\u2013279 (2021)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01591-5_2","volume-title":"Numerical Validation in Current Hardware Architectures","author":"UW Kulisch","year":"2009","unstructured":"Kulisch, U.W.: Complete interval arithmetic and its implementation on the computer. In: Cuyt, A., Kr\u00e4mer, W., Luther, W., Markstein, P. (eds.) Numerical Validation in Current Hardware Architectures. LNCS, vol. 5492, pp. 7\u201326. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01591-5_2"},{"issue":"1","key":"4_CR23","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1145\/2578855.2535857","volume":"49","author":"Y Li","year":"2014","unstructured":"Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with SMT solvers. SIGPLAN Not. 49(1), 607\u2013618 (2014)","journal-title":"SIGPLAN Not."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Marescotti, M., Hyv\u00e4rinen, A.E., Sharygina, N.: SMTS: Distributed, visualized constraint solving. In: LPAR, pp. 534\u2013542 (2018)","DOI":"10.29007\/fhgn"},{"key":"4_CR25","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"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-642-20398-5_22","volume-title":"NASA Formal Methods","author":"J Peleska","year":"2011","unstructured":"Peleska, J., Vorobev, E., Lapschies, F.: Automated test case generation with SMT-solving and abstract interpretation. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 298\u2013312. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_22"},{"key":"4_CR27","unstructured":"Reisenberger, C.: PBoolector: a parallel SMT solver for QF_BV by combining bit-blasting with look-ahead. Ph.D. thesis, Master\u2019s thesis, Johannes Kepler Univesit\u00e4t Linz, Linz, Austria (2014)"},{"key":"4_CR28","unstructured":"Schupp, S., \u00c1brah\u00e1m, E., Rossmanith, P., Loup, D.I.U.: Interval constraint propagation in SMT compliant decision procedures. Master\u2019s thesis, RWTH Aachen (2013)"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Shinano, Y., Achterberg, T., Berthold, T., Heinz, S., Koch, T., Winkler, M.: Solving open MIP instances with paraSCIP on supercomputers using up to 80,000 cores. In: 2016 IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 770\u2013779 (2016). https:\/\/doi.org\/10.1109\/IPDPS.2016.56","DOI":"10.1109\/IPDPS.2016.56"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Shinano, Y., Heinz, S., Vigerske, S., Winkler, M.: Fiberscip-a shared memory parallelization of scip. INFORMS J. Comput. 30(1), 11\u201330 (2018)","DOI":"10.1287\/ijoc.2017.0762"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Steiner, W.: An evaluation of SMT-based schedule synthesis for time-triggered multi-hop networks. In: 2010 31st IEEE Real-Time Systems Symposium, pp. 375\u2013384 (2010)","DOI":"10.1109\/RTSS.2010.25"},{"key":"4_CR32","unstructured":"Wilson, A., Noetzli, A., Reynolds, A., Cook, B., Tinelli, C., Barrett, C.W.: Partitioning strategies for distributed SMT solving. In: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp. 199\u2013208 (2023)"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"715","DOI":"10.1007\/978-3-642-02658-4_60","volume-title":"Computer Aided Verification","author":"CM Wintersteiger","year":"2009","unstructured":"Wintersteiger, C.M., Hamadi, Y., de Moura, L.: A concurrent portfolio approach to SMT solving. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 715\u2013720. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_60"}],"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-65627-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T21:17:46Z","timestamp":1732483066000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}