{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:29:17Z","timestamp":1743110957472,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711619"},{"type":"electronic","value":"9783031711626"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"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><jats:p>MaxSAT modulo theories (MaxSMT) is an important generalization of Satisfiability modulo theories (SMT) with various applications. In this paper, we focus on MaxSMT with the background theory of Linear Integer Arithmetic, denoted as MaxSMT(LIA). We design the first local search algorithm for MaxSMT(LIA) called PairLS, based on the following novel ideas. A novel operator called <jats:italic>pairwise<\/jats:italic> operator is proposed for integer variables. It extends the original local search operator by simultaneously operating on two variables, enriching the search space. Moreover, a compensation-based picking heuristic is proposed to determine and distinguish the <jats:italic>pairwise<\/jats:italic> operations. Experiments are conducted to evaluate our algorithm on massive benchmarks. The results show that our solver is competitive with state-of-the-art MaxSMT solvers. Furthermore, we also apply the <jats:italic>pairwise<\/jats:italic> operation to enhance the local search algorithm of SMT, which shows its extensibility.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_3","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"55-72","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Local Search Algorithm for\u00a0MaxSMT(LIA)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-0730-1388","authenticated-orcid":false,"given":"Xiang","family":"He","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1356-6057","authenticated-orcid":false,"given":"Bohan","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8436-3532","authenticated-orcid":false,"given":"Mengyu","family":"Zhao","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1730-6922","authenticated-orcid":false,"given":"Shaowei","family":"Cai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-030-53288-8_10","volume-title":"Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Proceedings, Part I","author":"E Albert","year":"2020","unstructured":"Albert, E., Gordillo, P., Rubio, A., Schett, M.A.: Synthesis of super-optimized smart contracts using Max-SMT. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Proceedings, Part I, pp. 177\u2013200. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_10"},{"key":"3_CR2","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/j.artint.2013.01.002","volume":"196","author":"C Ans\u00f3tegui","year":"2013","unstructured":"Ans\u00f3tegui, C., Bonet, M.L., Levy, J.: Sat-based MaxSAT algorithms. Artif. Intell. 196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Balint, A., Sch\u00f6ning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. In: Proceedings of SAT 2012, pp. 16\u201329 (2012)","DOI":"10.1007\/978-3-642-31612-8_3"},{"key":"3_CR4","unstructured":"Biere, A., Splatz, L., Plingeling, T.: YalSAT entering the SAT competition 2016. In: Proceedings of SAT Competition 2016, pp. 44\u201345 (2016)"},{"key":"3_CR5","first-page":"1","volume":"30","author":"NS Bj\u00f8rner","year":"2014","unstructured":"Bj\u00f8rner, N.S., Phan, A.D.: $$\\nu $$z-maximal satisfaction with z3. Scss 30, 1\u20139 (2014)","journal-title":"Scss"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Larra, D., Oliveras, A., Rodr\u0131guez-Carbonell, E., Rubio, A.: Compositional safety verification with Max-SMT. In: 2015 Formal Methods in Computer-Aided Design (FMCAD), pp. 33\u201340. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542250"},{"key":"3_CR7","unstructured":"Cai, S.: Balance between complexity and quality: Local search for minimum vertex cover in massive graphs. In: Twenty-Fourth International Joint Conference on Artificial Intelligence, pp. 747\u2013753 (2015)"},{"key":"3_CR8","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2020.103354","volume":"287","author":"S Cai","year":"2020","unstructured":"Cai, S., Lei, Z.: Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability. Artif. Intell. 287, 103354 (2020)","journal-title":"Artif. Intell."},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-031-13188-2_12","volume-title":"Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part II","author":"S Cai","year":"2022","unstructured":"Cai, S., Li, B., Zhang, X.: Local search for\u00a0SMT on\u00a0linear integer arithmetic. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification: 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part II, pp. 227\u2013248. Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_12"},{"issue":"4","key":"3_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3597495","volume":"24","author":"S Cai","year":"2023","unstructured":"Cai, S., Li, B., Zhang, X.: Local search for satisfiability modulo integer arithmetic theories. ACM Trans. Comput. Log. 24(4), 1\u201326 (2023)","journal-title":"ACM Trans. Comput. Log."},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-24318-4_1","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"S Cai","year":"2015","unstructured":"Cai, S., Luo, C., Su, K.: CCAnr: a configuration checking based local search solver for non-random satisfiability. In: Heule, M., Weaver, S. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2015, pp. 1\u20138. Springer International Publishing, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_1"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.artint.2013.09.001","volume":"204","author":"S Cai","year":"2013","unstructured":"Cai, S., Su, K.: Local search for Boolean satisfiability with configuration checking and subscore. Artif. Intell. 204, 75\u201398 (2013)","journal-title":"Artif. Intell."},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability modulo the theory of costs: foundations and applications. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 99\u2013113. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_8"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-39071-5_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2013","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: A modular approach to MaxSAT modulo theories. In: J\u00e4rvisalo, M., Van Gelder, A. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2013, pp. 150\u2013165. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39071-5_12"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-319-94205-6_10","volume-title":"Automated Reasoning","author":"K Fazekas","year":"2018","unstructured":"Fazekas, K., Bacchus, F., Biere, A.: Implicit hitting set algorithms for maximum satisfiability modulo theories. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning, pp. 134\u2013151. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_10"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Fr\u00f6hlich, A., Biere, A., Wintersteiger, C., Hamadi, Y.: Stochastic local search for satisfiability modulo theories. In: Proceedings of AAAI 2015, vol.\u00a029 (2015)","DOI":"10.1609\/aaai.v29i1.9372"},{"key":"3_CR17","unstructured":"He, X., Li, B., Zhao, M., Cai, S.: A local search algorithm for MaxSMT(LIA) (2024). https:\/\/arxiv.org\/abs\/2406.15782"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"53","DOI":"10.3233\/SAT190116","volume":"11","author":"A Ignatiev","year":"2019","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient MaxSAT solver. J. Satisfiability, Boolean Model. Comput. 11(1), 53\u201364 (2019)","journal-title":"J. Satisfiability, Boolean Model. Comput."},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Larraz, D., Nimkar, K., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving non-termination using Max-SMT. In: Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings 26, pp. 779\u2013796. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_52","DOI":"10.1007\/978-3-319-08867-9_52"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Lei, Z., Cai, S.: Solving (weighted) partial MaxSAT by dynamic local search for sat. In: IJCAI, vol.\u00a07, pp. 1346\u201352 (2018)","DOI":"10.24963\/ijcai.2018\/187"},{"key":"3_CR21","unstructured":"Li, B., Cai, S.: Local search for SMT on linear and multilinear real arithmetic. arXiv preprint arXiv:2303.06676 (2023)"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Li, C.M., Li, Y.: Satisfying versus falsifying in local search for satisfiability. In: Proceedings of SAT 2012, pp. 477\u2013478 (2012)","DOI":"10.1007\/978-3-642-31612-8_43"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Li, C.M., Manya, F.: MaxSAT, hard and soft constraints. In: Handbook of satisfiability, pp. 903\u2013927. IOS Press (2021)","DOI":"10.3233\/FAIA201007"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Li, C.M., Xu, Z., Coll, J., Many\u00e0, F., Habet, D., He, K.: Combining clause learning and branch and bound for MaxSAT. In: 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2021)","DOI":"10.24963\/ijcai.2022\/739"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Li, H., Xia, B., Zhao, T.: Local search for solving satisfiability of polynomial formulas. arXiv preprint arXiv:2303.09072 (2023)","DOI":"10.1007\/978-3-031-37703-7_5"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-319-09284-3_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"R Martins","year":"2014","unstructured":"Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver,. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438\u2013445. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_33"},{"key":"3_CR27","unstructured":"Niemetz, A., Preiner, M.: Ternary propagation-based local search for more bit-precise reasoning. In: 2020 Formal Methods in Computer Aided Design (FMCAD), pp. 214\u2013224 (2020)"},{"key":"3_CR28","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-319-41528-4_11","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I","author":"A Niemetz","year":"2016","unstructured":"Niemetz, A., Preiner, M., Biere, A.: Precise and complete propagation based local search for satisfiability modulo theories. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, pp. 199\u2013217. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_11"},{"issue":"3","key":"3_CR29","doi-asserted-by":"publisher","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. Design 51(3), 608\u2013636 (2017)","journal-title":"Formal Methods Syst. Design"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A.: On sat modulo theories and optimization problems. In: Theory and Applications of Satisfiability Testing-SAT 2006: 9th International Conference, Seattle, WA, USA, August 12-15, 2006. Proceedings 9, pp. 156\u2013169. Springer (2006). https:\/\/doi.org\/10.1007\/11814948_18","DOI":"10.1007\/11814948_18"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with ($$\\mathbb{Q}$$) cost functions. In: International Joint Conference on Automated Reasoning, pp. 484\u2013498. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_38","DOI":"10.1007\/978-3-642-31365-3_38"},{"issue":"2","key":"3_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699915","volume":"16","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Logic (TOCL) 16(2), 1\u201343 (2015)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"issue":"3","key":"3_CR33","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-09508-6","volume":"64","author":"R Sebastiani","year":"2020","unstructured":"Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. J. Autom. Reason. 64(3), 423\u2013460 (2020)","journal-title":"J. Autom. Reason."},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Terra-Neves, M., Machado, N., Lynce, I., Manquinho, V.: Concurrency debugging with MaxSMT. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a033, pp. 1608\u20131616 (2019)","DOI":"10.1609\/aaai.v33i01.33011608"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:52Z","timestamp":1725933772000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}