{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:11Z","timestamp":1750220831291,"version":"3.41.0"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T00:00:00Z","timestamp":1566000000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Research Council"},{"DOI":"10.13039\/501100003329","name":"Spanish Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"crossref","award":["TIN2015-69175-C4-3-R (Spanish MINECO\/FEDER UE)"],"award-info":[{"award-number":["TIN2015-69175-C4-3-R (Spanish MINECO\/FEDER UE)"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Spanish Ministerio de Ciencia, Innovaci\u00f3n y Universidades","award":["RTI2018-094403-B-C33 (Spanish MICINN\/FEDER UE)"],"award-info":[{"award-number":["RTI2018-094403-B-C33 (Spanish MICINN\/FEDER UE)"]}]},{"name":"European Union's Horizon 2020 research and innovation programme","award":["ERC-2014-CoG 648276 AUTAR"],"award-info":[{"award-number":["ERC-2014-CoG 648276 AUTAR"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"<jats:p>We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas with integer polynomial constraints. Following previous work, we propose to solve SMT(QF-NIA) instances by reducing them to linear arithmetic: non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. For variables that do not have a finite domain, we can artificially introduce one by imposing a lower and an upper bound and iteratively enlarge it until a solution is found (or the procedure times out).<\/jats:p>\n          <jats:p>The key for the success of the approach is to determine, at each iteration, which domains have to be enlarged. Previously, unsatisfiable cores were used to identify the domains to be changed, but no clue was obtained as to how large the new domains should be. Here, we explain two novel ways to guide this process by analyzing solutions to optimization problems: (i) to minimize the number of violated artificial domain bounds, solved via a Max-SMT solver, and (ii) to minimize the distance with respect to the artificial domains, solved via an Optimization Modulo Theories (OMT) solver. Using this SMT-based optimization technology allows smoothly extending the method to also solve Max-SMT problems over non-linear integer arithmetic. Finally, we leverage the resulting Max-SMT(QF-NIA) techniques to solve \u2203 \u2200 formulas in a fragment of quantified non-linear arithmetic that appears commonly in verification and synthesis applications.<\/jats:p>","DOI":"10.1145\/3340923","type":"journal-article","created":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T19:41:32Z","timestamp":1566243692000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers"],"prefix":"10.1145","volume":"20","author":[{"given":"Cristina","family":"Borralleras","sequence":"first","affiliation":[{"name":"Universitat de Vic\u2014Universitat Central de Catalunya, Vic, Spain"}]},{"given":"Daniel","family":"Larraz","sequence":"additional","affiliation":[{"name":"The University of Iowa, Iowa, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1061-3954","authenticated-orcid":false,"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[{"name":"Universitat Polit\u00e8cnica de Catalunya, Barcelona, Spain"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[{"name":"Universidad Complutense de Madrid, Madrid, Spain"}]}],"member":"320","published-online":{"date-parts":[[2019,8,17]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2013.01.002"},{"key":"e_1_2_1_2_1","first-page":"2","article-title":"Practical algorithms for unsatisfiability proof and core generation in SAT solvers","volume":"23","author":"Ach\u00e1 Roberto As\u00edn","year":"2010","journal-title":"AI Commun."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_2_1_4_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved from: www.SMT-LIB.org.  Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). Retrieved from: www.SMT-LIB.org."},{"volume-title":"Algorithms in Real Algebraic Geometry","author":"Basu S.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2350156.2350163"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02136172"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1119584.1644552"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535860"},{"key":"e_1_2_1_10_1","volume-title":"Frontiers in Artificial Intelligence and Applications","volume":"185","author":"Biere Armin","year":"2009"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/2832249.2832283"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Anh-Dung Phan and Lars Fleckenstein. 2015. vZ\u2014An optimizing SMT solver. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915). Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201915). (Lecture Notes in Computer Science) Christel Baier and Cesare Tinelli (Eds.) Vol. 9035. Springer 194--199.  Nikolaj Bj\u00f8rner Anh-Dung Phan and Lars Fleckenstein. 2015. v Z\u2014An optimizing SMT solver. In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201915). Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS\u201915). (Lecture Notes in Computer Science) Christel Baier and Cesare Tinelli (Eds.) Vol. 9035. Springer 194--199.","DOI":"10.1007\/978-3-662-46681-0_14"},{"volume-title":"In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201910)","year":"2010","author":"Bloem Roderick","key":"e_1_2_1_13_1"},{"key":"e_1_2_1_14_1","volume-title":"In Proceedings of the 24th International Conference on Automated Deduction (CADE\u201910)","volume":"7898","author":"Ed Maria Paola","year":"2013"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9196-8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2893529.2893541"},{"volume-title":"EFSMT: A logical framework for cyber-physical systems. Retrieved from: http:\/\/arxiv.org\/abs\/1306.3456.","year":"2013","author":"Cheng Chih-Hong","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_8"},{"volume-title":"Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Automata Theory and Formal Languages (Lecture Notes in Computer Science)","year":"1975","author":"Collins George E.","key":"e_1_2_1_19_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647771.734281"},{"volume-title":"Computability Theory","author":"Cooper S. Barry","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2034214.2034245"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_26"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_35"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.079"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_12"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0127-z"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"volume-title":"Proceedings of the 13th International Workshop on Satisfiability Modulo Theories (SMT\u201915)","year":"2015","author":"Dutertre Bruno","key":"e_1_2_1_32_1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_2_1_34_1","first-page":"3","article-title":"Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure","volume":"1","author":"Fr\u00e4nzle Martin","year":"2007","journal-title":"J. Sat., Boolean Model. Comput."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_25"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1768142.1768175"},{"volume-title":"Proceedings of the Conference on Formal Methods in Computer-Aided Design (FMCAD\u201909)","author":"Malay","key":"e_1_2_1_37_1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_23"},{"volume-title":"Proceedings of the International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201910)","author":"Gao Sicun","key":"e_1_2_1_39_1"},{"volume-title":"Proceedings of the International Conference on Automated Deduction (CADE\u201913)","author":"Gao Sicun","key":"e_1_2_1_40_1"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/2682923.2682943"},{"key":"e_1_2_1_42_1","first-page":"1","article-title":"A practical approach to satisability modulo linear integer arithmetic","volume":"8","author":"Griggio Alberto","year":"2012","journal-title":"J. Sat., Boolean Model. Comput."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_27"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40663-8_18"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/3077629.3077649"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.11.004"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22969-0_15"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_52"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_25"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_12"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9176-z"},{"volume-title":"Handbook of Satisfiability, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications","author":"Li Chu Min","key":"e_1_2_1_53_1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535857"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_8"},{"volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI\u201913)","year":"2013","author":"Marques-Silva Jo\u00e3o","key":"e_1_2_1_57_1"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-013-9146-2"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_18"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"volume-title":"Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201910)","author":"Nuzzo Pierluigi","key":"e_1_2_1_61_1"},{"volume-title":"Spain. (January","year":"2012","author":"Oliver Roc","key":"e_1_2_1_62_1"},{"key":"e_1_2_1_63_1","first-page":"04","article-title":"Gr\u00f6bner basis construction algorithms based on theorem proving saturation loops","volume":"18","author":"Passmore Grant Olney","year":"2010","journal-title":"Decision Procedures in Software, Hardware and Bioware"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0046-1"},{"volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","key":"e_1_2_1_67_1"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699915"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_27"},{"key":"e_1_2_1_70_1","volume-title":"Proceedings of the 19th European Conference on Artificial Intelligence (ECAI\u201910)","volume":"215","author":"Soh Takehide","year":"2010"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08587-6_28"},{"volume-title":"A decision method for elementary algebra and geometry. Bull. Amer. Math. Soc. 59","year":"1951","author":"Tarski Alfred","key":"e_1_2_1_72_1"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_33"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_16"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80003-8"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002000050055"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939168"},{"volume-title":"Proceedings of the Conference on Design, Automation and Test in Europe 1","year":"2003","author":"Zhang Lintao","key":"e_1_2_1_78_1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3340923","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3340923","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:32Z","timestamp":1750202012000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3340923"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,17]]},"references-count":78,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3340923"],"URL":"https:\/\/doi.org\/10.1145\/3340923","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,8,17]]},"assertion":[{"value":"2017-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-08-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}