{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:29Z","timestamp":1762459529370,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661667"},{"type":"electronic","value":"9783319661674"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_11","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T11:15:18Z","timestamp":1503918918000},"page":"189-206","source":"Crossref","is-referenced-by-count":10,"title":["Subtropical Satisfiability"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4700-6031","authenticated-orcid":false,"given":"Pascal","family":"Fontaine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8050-7228","authenticated-orcid":false,"given":"Mizuhito","family":"Ogawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8088-340X","authenticated-orcid":false,"given":"Thomas","family":"Sturm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2239-6574","authenticated-orcid":false,"given":"Xuan Tung","family":"Vu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"issue":"3","key":"11_CR1","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10817-009-9149-2","volume":"44","author":"B Akbarpour","year":"2010","unstructured":"Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175\u2013205 (2010)","journal-title":"J. Autom. Reason."},{"key":"11_CR2","unstructured":"Barrett, C., Kroening, D., Melham, T.: Problem solving for the 21st century: efficient solvers for satisfiability modulo theories. Technical Report 3, London Mathematical Society and Smith Institute for Industrial Mathematics and System Engineering Knowledge Transfer Report(2014)"},{"key":"11_CR3","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"11_CR4","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1016\/S1574-6526(06)80020-9","volume-title":"Handbook of Constraint Programming","author":"F Benhamou","year":"2006","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming, pp. 571\u2013604. Elsevier, New York (2006)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-70545-1_27","volume-title":"Computer Aided Verification","author":"M Bofill","year":"2008","unstructured":"Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: The barcelogic SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 294\u2013298. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-70545-1_27"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02959-2_12"},{"key":"11_CR7","unstructured":"Buchberger, B.: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Doctoral dissertation, University of Innsbruck, Austria (1965)"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-662-54577-5_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2017","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 58\u201375. Springer, Heidelberg (2017). doi: 10.1007\/978-3-662-54577-5_4"},{"key":"11_CR9","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. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442\u2013448. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31612-8_35"},{"key":"11_CR10","doi-asserted-by":"crossref","DOI":"10.1515\/9781400884179","volume-title":"Linear Programming and Extensions","author":"GB Dantzig","year":"1963","unstructured":"Dantzig, G.B.: Linear Programming and Extensions. Prentice University Press, Princeton (1963)"},{"key":"11_CR11","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). doi: 10.1007\/11817963_11"},{"key":"11_CR12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.jcp.2015.02.050","volume":"291","author":"H Errami","year":"2015","unstructured":"Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A.: Detection of Hopf bifurcations in chemical reaction networks using convex coordinates. J. Comput. Phys. 291, 279\u2013302 (2015)","journal-title":"J. Comput. Phys."},{"key":"11_CR13","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. J. Satisf. Boolean Model. Comput. 1, 209\u2013236 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"11_CR14","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. 4501, pp. 340\u2013354. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-72788-0_33"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Ganai, M., Ivancic, F.: Efficient decision procedure for non-linear arithmetic constraints using CORDIC. In: Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 61\u201368 (2009)","DOI":"10.1109\/FMCAD.2009.5351140"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175\u2013188. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27813-9_14"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: Formal Methods in Computer-Aided Design (FMCAD) 2013, pp. 105\u2013112 (2013)","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"11_CR18","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). doi: 10.1007\/978-3-642-38574-2_14"},{"key":"11_CR19","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1145\/1132973.1132980","volume":"32","author":"L Granvilliers","year":"2006","unstructured":"Granvilliers, L., Benhamou, F.: RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans. Math. Softw. 32, 138\u2013156 (2006)","journal-title":"ACM Trans. Math. Softw."},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","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, vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_27"},{"issue":"4","key":"11_CR21","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF02579150","volume":"4","author":"N Karmarkar","year":"1984","unstructured":"Karmarkar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4(4), 373\u2013395 (1984)","journal-title":"Combinatorica"},{"issue":"1","key":"11_CR22","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0041-5553(80)90061-0","volume":"20","author":"L Khachiyan","year":"1980","unstructured":"Khachiyan, L.: Polynomial algorithms in linear programming. USSR Comput. Math. Math. Phys. 20(1), 53\u201372 (1980)","journal-title":"USSR Comput. Math. Math. Phys."},{"key":"11_CR23","unstructured":"Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, School of Informatics, University of Edinburgh (2011)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-02614-0_14","volume-title":"Intelligent Computer Mathematics","author":"GO Passmore","year":"2009","unstructured":"Passmore, G.O., Jackson, P.B.: Combined decision techniques for the existential theory of the reals. In: Carette, J., Dixon, L., Coen, C.S., Watt, S.M. (eds.) CICM 2009. LNCS, vol. 5625, pp. 122\u2013137. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02614-0_14"},{"key":"11_CR25","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1145\/1183278.1183282","volume":"7","author":"S Ratschan","year":"2006","unstructured":"Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log. 7, 723\u2013748 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"11_CR26","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Sturm, T.: Subtropical real root finding. In: Proceedings of the ISSAC 2015, pp. 347\u2013354. ACM (2015)","DOI":"10.1145\/2755996.2756677"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40229-1_16","volume-title":"Automated Reasoning","author":"VX Tung","year":"2016","unstructured":"Tung, V.X., Van Khanh, T., Ogawa, M.: raSAT: an SMT solver for polynomial constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 228\u2013237. Springer, Cham (2016). doi: 10.1007\/978-3-319-40229-1_16"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","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\u00a0arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6355, pp. 481\u2013500. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_27"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66167-4_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T03:52:42Z","timestamp":1750823562000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}