{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T03:49:18Z","timestamp":1780631358075,"version":"3.54.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,3,15]],"date-time":"2013-03-15T00:00:00Z","timestamp":1363305600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s10817-013-9281-x","type":"journal-article","created":{"date-parts":[[2013,3,14]],"date-time":"2013-03-14T02:26:38Z","timestamp":1363227998000},"page":"79-108","source":"Crossref","is-referenced-by-count":24,"title":["Cutting to the Chase"],"prefix":"10.1007","volume":"51","author":[{"given":"Dejan","family":"Jovanovi\u0107","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leonardo","family":"de Moura","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2013,3,15]]},"reference":[{"key":"9281_CR1","unstructured":"Achterberg, T.: SCIP: Solving constraint integer programs. PhD thesis, TU Berlin (2007)"},{"issue":"4","key":"9281_CR2","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/j.orl.2005.07.009","volume":"34","author":"T Achterberg","year":"2003","unstructured":"Achterberg, T., Koch, T., Martin, A.: MIPLIB 2003. Oper. Res. Lett. 34(4), 361\u2013372 (2006)","journal-title":"Oper. Res. Lett."},{"key":"9281_CR3","unstructured":"Barth, P.: A Davis\u2013Putnam Based Enumeration Algorithm for Linear Pseudo-Boolean Optimization. Research Report MPI-I-95-2-003, Saarbr\u00fccken (1995)"},{"key":"9281_CR4","doi-asserted-by":"crossref","unstructured":"Berezin, S., Ganesh, V., Dill, D.L.: An online proof-producing decision procedure for mixed-integer linear arithmetic. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol.\u00a02619, pp.\u00a0521\u2013536. Springer (2003)","DOI":"10.1007\/3-540-36577-X_38"},{"key":"9281_CR5","first-page":"59","volume":"7","author":"D Berre Le","year":"2010","unstructured":"Le Berre, D., Parrain, A.: The Sat4j library, release 2.2 system description. JSAT 7, 59\u201364 (2010)","journal-title":"JSAT"},{"issue":"3","key":"9281_CR6","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1109\/TCAD.2004.842808","volume":"24","author":"D Chai","year":"2005","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-boolean constraint solver. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 24(3), 305\u2013317 (2005)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"issue":"4","key":"9281_CR7","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1016\/0012-365X(73)90167-2","volume":"4","author":"V Chv\u00e1tal","year":"1973","unstructured":"Chv\u00e1tal, V. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Math. 4(4), 305\u2013337 (1973)","journal-title":"Discrete Math."},{"issue":"91\u201399","key":"9281_CR8","first-page":"300","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C. Theorem proving in arithmetic without multiplication. Mach. intell. 7(91\u201399), 300 (1972)","journal-title":"Mach. intell."},{"key":"9281_CR9","doi-asserted-by":"crossref","unstructured":"Cotton, S.: Natural domain SMT: a preliminary assessment. In: FORMATS (2010)","DOI":"10.1007\/978-3-642-15297-9_8"},{"issue":"7","key":"9281_CR10","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"9281_CR11","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM (JACM) 7(3), 201\u2013215 (1960)","journal-title":"J. ACM (JACM)"},{"key":"9281_CR12","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS 2008, Budapest, Hungary. LNCS, vol.\u00a04963, p.\u00a0337. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9281_CR13","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Verification, Model Checking, and Abstract Interpretation. LNCS, vol.\u00a07737, pp.\u00a01\u201312. Springer (2013)","DOI":"10.1007\/978-3-642-35873-9_1"},{"key":"9281_CR14","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV (2009)","DOI":"10.1007\/978-3-642-02658-4_20"},{"key":"9281_CR15","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de\u00a0Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, pp.\u00a081\u201394 (2006)","DOI":"10.1007\/11817963_11"},{"issue":"5","key":"9281_CR16","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1090\/S0002-9904-1958-10224-4","volume":"64","author":"RE Gomory","year":"1958","unstructured":"Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Am. Math. Soc. 64(5), 275\u2013278 (1958)","journal-title":"Bull. Am. Math. Soc."},{"key":"9281_CR17","unstructured":"Griggio, A.: A practical approach to SMT(LA(Z)). In: SMT Workshop (2010)"},{"key":"9281_CR18","doi-asserted-by":"crossref","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Principles and Practice of Constraint Programming (2009)","DOI":"10.1007\/978-3-642-04244-7_41"},{"key":"9281_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to richer logics. In: CAV (2009)","DOI":"10.1007\/978-3-642-02658-4_35"},{"key":"9281_CR20","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"issue":"6","key":"9281_CR21","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 DPLL procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"4","key":"9281_CR22","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"},{"key":"9281_CR23","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The omega test: a fast and practical integer programming algorithm for dependence analysis. In: ACM\/IEEE Conference on Supercomputing (1991)","DOI":"10.1145\/125826.125848"},{"key":"9281_CR24","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding quantifier-free Presburger formulas using parameterized solution bounds. In: Logic in Computer Science, pp.\u00a0100\u2013109. IEEE (2004)","DOI":"10.21236\/ADA461078"},{"key":"9281_CR25","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: ICCAD (1997)"},{"key":"9281_CR26","volume-title":"Integer and Combinatorial Optimization","author":"LA Wolsey","year":"1999","unstructured":"Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. Wiley, New\u00a0York (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9281-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9281-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9281-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T20:00:25Z","timestamp":1562788825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9281-x"}},"subtitle":["Solving Linear Integer Arithmetic"],"short-title":[],"issued":{"date-parts":[[2013,3,15]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["9281"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9281-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,3,15]]}}}