{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:43:54Z","timestamp":1777347834809,"version":"3.51.4"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319402284","type":"print"},{"value":"9783319402291","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_16","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"228-237","source":"Crossref","is-referenced-by-count":12,"title":["raSAT: An SMT Solver for Polynomial Constraints"],"prefix":"10.1007","author":[{"given":"Vu Xuan","family":"Tung","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"To","family":"Van Khanh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mizuhito","family":"Ogawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"16_CR1","unstructured":"Alliot, J.M., Gotteland, J.B., Vanaret, C., Durand, N., Gianazza, D.: Implementing an interval computation library for OCaml on x86\/amd64 architectures. In: ICFP. ACM (2012)"},{"key":"16_CR2","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: van Beek, P., Rossi, F., Walsh, T. (eds.) Handbook of Constraint Programming, pp. 571\u2013604. Elsevier, Amsterdam (2006)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"16_CR4","unstructured":"Comba, J.L.D., Stolfi, J.: Affine arithmetic and its applications to computer graphics. In: SIBGRAPI 1993, pp. 9\u201318 (1993)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"16_CR7","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 1, 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Ganai, M., Ivancic, F.: Efficient decision procedure for non-linear arithmetic constraints using cordic. In: FMCAD 2009, pp. 61\u201368, November 2009","DOI":"10.1109\/FMCAD.2009.5351140"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo odes. In: FMCAD 2013, pp. 105\u2013112, October 2013","DOI":"10.1109\/FMCAD.2013.6679398"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.: $${\\sf dReal}$$ : an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"key":"16_CR11","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."},{"issue":"5","key":"16_CR12","doi-asserted-by":"crossref","first-page":"1038","DOI":"10.1145\/502102.502106","volume":"48","author":"T Hickey","year":"2001","unstructured":"Hickey, T., Ju, Q., Van Emden, M.H.: Interval arithmetic: from principles to implementation. J. ACM 48(5), 1038\u20131068 (2001)","journal-title":"J. ACM"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Khanh, T.V., Ogawa, M.: SMT for polynomial constraints on real numbers. In: TAPAS 2012. ENTCS, vol. 289, pp. 27\u201340 (2012)","DOI":"10.1016\/j.entcs.2012.11.004"},{"issue":"11","key":"16_CR15","first-page":"992","volume":"8","author":"F Messine","year":"2002","unstructured":"Messine, F.: Extentions of affine arithmetic: application to unconstrained global optimization. J. UCS 8(11), 992\u20131015 (2002)","journal-title":"J. UCS"},{"key":"16_CR16","series-title":"Prentice-Hall Series in Automatic Computation","volume-title":"Interval Analysis","author":"R Moore","year":"1966","unstructured":"Moore, R.: Interval Analysis. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Upper Saddle River (1966)"},{"key":"16_CR17","volume-title":"Interval Methods for Systems of Equations","author":"A Neumaier","year":"1990","unstructured":"Neumaier, A.: Interval Methods for Systems of Equations. Cambridge Middle East Library. Cambridge University Press, Cambridge (1990)"},{"key":"16_CR18","unstructured":"Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, School of Informatics, University of Edinburgh (2011)"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) MKM 2009, Held as Part of CICM 2009. LNCS, vol. 5625, pp. 122\u2013137. Springer, Heidelberg (2009)"},{"issue":"4","key":"16_CR20","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. Logic 7(4), 723\u2013748 (2006)","journal-title":"ACM Trans. Comput. Logic"},{"key":"16_CR21","series-title":"Symbolic Computation","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"G Tseitin","year":"1983","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. Symbolic Computation, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"16_CR22","unstructured":"Tung, V.X., Khanh, T.V., Ogawa, M.: raSAT: SMT for polynomial inequality. In: SMT Workshop 2014, p. 67 (2014)"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 irrational arithmetic. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 481\u2013500. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T21:28:47Z","timestamp":1748986127000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}