{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:10Z","timestamp":1725511990564},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797180"},{"type":"electronic","value":"9783540797197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79719-7_8","type":"book-chapter","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T04:04:57Z","timestamp":1210046697000},"page":"77-90","source":"Crossref","is-referenced-by-count":17,"title":["SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers"],"prefix":"10.1007","author":[{"given":"Germain","family":"Faure","sequence":"first","affiliation":[]},{"given":"Robert","family":"Nieuwenhuis","sequence":"additional","affiliation":[]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[]},{"given":"Enric","family":"Rodr\u00edguez-Carbonell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/11532231_23","volume-title":"Automated Deduction \u2013 CADE-20","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: The MathSAT 3 System. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 315\u2013321. Springer, Heidelberg (2005)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"8_CR3","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT Solver. Technical report, SRI International (2006), Available at http:\/\/yices.csl.sri.com"},{"key":"8_CR4","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)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bjorner, N.: Z3: An Efficient SMT Solver. Technical report, Microsoft Research, Redmon (2007), Available at http:\/\/research.microsoft.com\/projects\/z3","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"8_CR6","unstructured":"ILOG. ILOG CPLEX v.11 (2007), http:\/\/www.ilog.com\/products\/cplex"},{"key":"8_CR7","unstructured":"Makhorin, A.: GLPK 4.25 (GNU Linear Programming Kit) (2007), Available at http:\/\/www.gnu.org\/software\/glpk\/"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1016\/0377-2217(86)90215-8","volume":"23","author":"I. Maros","year":"1986","unstructured":"Maros, I.: A general Phase-I method in linear programming. European Journal of Operational Research\u00a023(1), 64\u201377 (1986)","journal-title":"European Journal of Operational Research"},{"key":"8_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/11591191_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Decision Procedures for SAT, SAT Modulo Theories and Beyond. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 23\u201346. Springer, Heidelberg (2005)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"issue":"6","key":"8_CR11","doi-asserted-by":"crossref","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). Journal of the ACM, JACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM, JACM"},{"key":"8_CR12","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1987)"},{"key":"8_CR13","unstructured":"Tinelli, C., Ranise, S.: SMT-LIB: The Satisfiability Modulo Theories Library (2005), http:\/\/goedel.cs.uiowa.edu\/smtlib\/"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/11814948_17","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"Y. Yu","year":"2006","unstructured":"Yu, Y., Malik, S.: Lemma Learning in SMT on Linear Constraints. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 142\u2013155. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79719-7_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:29:16Z","timestamp":1619508556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79719-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797180","9783540797197"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79719-7_8","relation":{},"subject":[]}}