{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:05Z","timestamp":1747592465361},"publisher-location":"Cham","reference-count":50,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319092836"},{"type":"electronic","value":"9783319092843"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-09284-3_25","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T09:43:21Z","timestamp":1404294201000},"page":"333-350","source":"Crossref","is-referenced-by-count":14,"title":["Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Larraz","sequence":"first","affiliation":[]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","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.\u00a0196, 77\u2013105 (2013)","journal-title":"Artif. Intell."},{"key":"25_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-05355-3","volume-title":"Algorithms in Real Algebraic Geometry","author":"S. Basu","year":"2003","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Springer, Berlin (2003)"},{"issue":"2","key":"25_CR3","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A. Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"issue":"1","key":"25_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/BF02136172","volume":"18","author":"R. Ben-Eliyahu","year":"1996","unstructured":"Ben-Eliyahu, R., Dechter, R.: On computing minimal models. Ann. Math. Artif. Intell.\u00a018(1), 3\u201327 (1996)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"25_CR5","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.artint.2005.06.003","volume":"169","author":"R. Ben-Eliyahu-Zohary","year":"2005","unstructured":"Ben-Eliyahu-Zohary, R.: An incremental algorithm for generating all minimal models. Artif. Intell.\u00a0169(1), 1\u201322 (2005)","journal-title":"Artif. Intell."},{"key":"25_CR6","first-page":"221","volume-title":"Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014","author":"T. Beyene","year":"2014","unstructured":"Beyene, T., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 221\u2013233. ACM, New York (2014)"},{"key":"25_CR7","unstructured":"Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185. IOS Press (February 2009)"},{"key":"25_CR8","unstructured":"Bloem, R., Sharygina, N. (eds.): Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23. IEEE (2010)"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Bockmayr, A., Weispfenning, V.: Solving numerical constraints. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 751\u2013842. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50014-X"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction","year":"2013","unstructured":"Bonacina, M.P. (ed.): CADE 2013. LNCS, vol.\u00a07898. Springer, Heidelberg (2013)"},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10817-010-9196-8","volume":"48","author":"C. Borralleras","year":"2012","unstructured":"Borralleras, C., Lucas, S., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reasoning\u00a048(1), 107\u2013131 (2012)","journal-title":"J. Autom. Reasoning"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M. Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 413\u2013429. Springer, Heidelberg (2013)"},{"key":"25_CR14","unstructured":"Cheng, C.H., Shankar, N., Ruess, H., Bensalem, S.: EFSMT: A Logical Framework for Cyber-Physical Systems, coRR abs\/1306.3456 (2013)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability Modulo the Theory of Costs: Foundations and Applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 99\u2013113. Springer, Heidelberg (2010)"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"25_CR18","unstructured":"Cooper, S.B.: Computability Theory. Chapman Hall\/CRC Mathematics Series (2004)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/978-3-642-31612-8_35","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"F. Corzilius","year":"2012","unstructured":"Corzilius, F., Loup, U., Junges, S., \u00c1brah\u00e1m, E.: SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox - (Tool Presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 442\u2013448. Springer, Heidelberg (2012)"},{"key":"25_CR20","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.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"issue":"3-4","key":"25_CR21","first-page":"209","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT\u00a01(3-4), 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"25_CR22","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.\u00a04501, pp. 340\u2013354. Springer, Heidelberg (2007)"},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ivancic, F.: Efficient decision procedure for non-linear arithmetic constraints using CORDIC. In: FMCAD, pp. 61\u201368. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351140"},{"key":"25_CR24","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S. Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: \u03b4-complete decision procedures for satisfiability over the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 286\u2013300. Springer, Heidelberg (2012)"},{"key":"25_CR25","unstructured":"Gao, S., Ganai, M.K., Ivancic, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In: Bloem and Sharygina [8], pp. 81\u201389"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: An SMT Solver for Nonlinear Theories over the Reals. In: Bonacina [10], pp. 208\u2013214","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/978-3-642-28756-5_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Grebenshchikov","year":"2012","unstructured":"Grebenshchikov, S., Gupta, A., Lopes, N.P., Popeea, C., Rybalchenko, A.: HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 549\u2013551. Springer, Heidelberg (2012)"},{"key":"25_CR28","series-title":"LNAI","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.\u00a07364, pp. 339\u2013354. Springer, Heidelberg (2012)"},{"key":"25_CR29","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.entcs.2012.11.004","volume":"289","author":"T.V. Khanh","year":"2012","unstructured":"Khanh, T.V., Ogawa, M.: SMT for Polynomial Constraints on Real Numbers. Electr. Notes Theor. Comput. Sci.\u00a0289, 27\u201340 (2012)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: FMCAD, pp. 218\u2013225. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"25_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35873-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Larraz","year":"2013","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-Based Array Invariant Generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 169\u2013188. Springer, Heidelberg (2013)"},{"key":"25_CR32","unstructured":"Li, C.M., Many\u00e0, F.: MaxSAT, Hard and Soft Constraints. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 613\u2013631. IOS Press (2009)"},{"key":"25_CR33","unstructured":"Marques-Silva, J., Heras, F., Janota, M., Previti, A., Belov, A.: On computing minimal correction subsets. In: Rossi, F. (ed.) IJCAI. IJCAI\/AAAI (2013)"},{"issue":"4","key":"25_CR34","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-013-9146-2","volume":"18","author":"A. Morgado","year":"2013","unstructured":"Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints\u00a018(4), 478\u2013534 (2013)","journal-title":"Constraints"},{"key":"25_CR35","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. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"25_CR36","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. Moura de","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.\u00a07737, pp. 1\u201312. Springer, Heidelberg (2013)"},{"key":"25_CR37","unstructured":"Moura, L.M.d., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina [10], pp. 178\u2013192"},{"key":"25_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 156\u2013169. Springer, Heidelberg (2006)"},{"issue":"6","key":"25_CR39","doi-asserted-by":"publisher","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\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"25_CR40","unstructured":"Nuzzo, P., Puggelli, A., Seshia, S.A., Sangiovanni-Vincentelli, A.L.: CalCS: SMT solving for non-linear convex constraints. In: Bloem and Sharygina [8], pp. 71\u201379"},{"key":"25_CR41","unstructured":"Oliver, R.: Optimization Modulo Theories. Master\u2019s thesis. Universitat Polit\u00e8cnica de Catalunya, Spain (January 2012)"},{"key":"25_CR42","doi-asserted-by":"crossref","unstructured":"Platzer, A., Quesel, J.-D., R\u00fcmmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol.\u00a05663, pp. 485\u2013501. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02959-2_35"},{"key":"25_CR43","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Jones, N.D., Leroy, X. (eds.) POPL, pp. 318\u2013329. ACM (2004)","DOI":"10.1145\/982962.964028"},{"issue":"1","key":"25_CR44","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods in System Design\u00a032(1), 25\u201355 (2008)","journal-title":"Formal Methods in System Design"},{"key":"25_CR45","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley (June 1998)"},{"key":"25_CR46","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1007\/978-3-642-31365-3_38","volume-title":"Automated Reasoning","author":"R. Sebastiani","year":"2012","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with $\\mathcal{LA}\\mathbb{(Q)}$ Cost Functions. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol.\u00a07364, pp. 484\u2013498. Springer, Heidelberg (2012)"},{"key":"25_CR47","unstructured":"Soh, T., Inoue, K.: Identifying necessary reactions in metabolic pathways by minimal model generation. In: Coelho, H., Studer, R., Wooldridge, M. (eds.) ECAI. Frontiers in Artificial Intelligence and Applications, vol.\u00a0215, pp. 277\u2013282. IOS Press (2010)"},{"key":"25_CR48","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Bulletin of the American Mathematical Society 59 (1951)","DOI":"10.1525\/9780520348097"},{"key":"25_CR49","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-642-17511-4_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H. Zankl","year":"2010","unstructured":"Zankl, H., Middeldorp, A.: Satisfiability of non-linear (ir)rational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS (LNAI), vol.\u00a06355, pp. 481\u2013500. Springer, Heidelberg (2010)"},{"key":"25_CR50","unstructured":"Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: 2008 Design, Automation and Test in Europe, vol.\u00a01, p. 10880 (2003)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-09284-3_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,10]],"date-time":"2022-04-10T09:28:24Z","timestamp":1649582904000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-09284-3_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319092836","9783319092843"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-09284-3_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}