{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T04:57:21Z","timestamp":1725857841674},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"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_9","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"116-132","source":"Crossref","is-referenced-by-count":11,"title":["Fast Cube Tests for LIA Constraint Solving"],"prefix":"10.1007","author":[{"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/978-3-642-31365-3_8","volume-title":"Automated Reasoning","author":"F Bobot","year":"2012","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Mahboubi, A., Mebsout, A., Melquiond, G.: A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 67\u201381. Springer, Heidelberg (2012)"},{"key":"9_CR3","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"S Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"623","DOI":"10.1007\/978-3-319-21401-6_42","volume-title":"Automated Deduction - CADE-25","author":"M Bromberger","year":"2015","unstructured":"Bromberger, M., Sturm, T., Weidenbach, C.: Linear integer arithmetic revisited. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25. LNCS, vol. 9195, pp. 623\u2013637. Springer, Heidelberg (2015)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-642-02658-4_20","volume-title":"Computer Aided Verification","author":"I Dillig","year":"2009","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 233\u2013247. Springer, Heidelberg (2009)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Heidelberg (2014)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"9_CR10","unstructured":"Ehrgott, M.: Scalarization techniques. In: Multicriteria Optimization, pp. 97\u2013126. Springer, Heidelberg (2005)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-3-540-79719-7_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"G Faure","year":"2008","unstructured":"Faure, G., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: SAT modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77\u201390. Springer, Heidelberg (2008)"},{"issue":"(1\/2)","key":"9_CR12","first-page":"1","volume":"8","author":"A Griggio","year":"2012","unstructured":"Griggio, A.: A practical approach to satisfiability modulo linear integer arithmetic. JSAT 8((1\/2)), 1\u201327 (2012)","journal-title":"JSAT"},{"issue":"4","key":"9_CR13","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1287\/opre.17.4.600","volume":"17","author":"FS Hillier","year":"1969","unstructured":"Hillier, F.S.: Efficient heuristic procedures for integer linear programming with an interior. Oper. Res. 17(4), 600\u2013637 (1969)","journal-title":"Oper. Res."},{"issue":"1","key":"9_CR14","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/s10817-013-9281-x","volume":"51","author":"D Jovanovi\u0107","year":"2013","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the chase. JAR 51(1), 79\u2013108 (2013)","journal-title":"JAR"},{"volume-title":"50 Years of Integer Programming 1958\u20132008: From the Early Years to the State-of-the-Art","year":"2010","key":"9_CR15","unstructured":"J\u00fcnger, M., Liebling, T.M., Naddef, D., Nemhauser, G.L., Pulleyblank, W.R., Reinelt, G., Rinaldi, G., Wolsey, L.A. (eds.): 50 Years of Integer Programming 1958\u20132008: From the Early Years to the State-of-the-Art. Springer, Heidelberg (2010)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-17179-7_12","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"R Kannan","year":"1986","unstructured":"Kannan, R., Lov\u00e1sz, L.: Covering minima and lattice point free convex bodies. In: Nori, K. (ed.) FSTTCS. LNCS, vol. 241, pp. 193\u2013213. Springer, Heidelberg (1986)"},{"issue":"4","key":"9_CR17","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\u2013396 (1984)","journal-title":"Combinatorica"},{"issue":"4","key":"9_CR18","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"CH Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765\u2013768 (1981)","journal-title":"J. ACM"}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T16:12:43Z","timestamp":1498320763000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}