{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:16:21Z","timestamp":1757312181414,"version":"3.37.3"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2017,5,8]],"date-time":"2017-05-08T00:00:00Z","timestamp":1494201600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Max Planck Institute for Informatics"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10703-017-0278-7","type":"journal-article","created":{"date-parts":[[2017,5,8]],"date-time":"2017-05-08T09:53:56Z","timestamp":1494237236000},"page":"433-461","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["New techniques for linear arithmetic: cubes and equalities"],"prefix":"10.1007","volume":"51","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-2190","authenticated-orcid":false,"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":[[2017,5,8]]},"reference":[{"key":"278_CR1","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway C, Deters M, Hadarean L, Jovanovi\u0107 D, King T, Reynolds A, Tinelli C (2011) CVC4. In: CAV, LNCS, vol 6806, pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"278_CR2","doi-asserted-by":"crossref","unstructured":"Beale EML (1954) An alternative method for linear programming, vol 50, issue 4, pp 513\u2013523","DOI":"10.1017\/S0305004100029650"},{"key":"278_CR3","unstructured":"Bj\u00f8rner N (1999) Integrating decision procedures for temporal verification. Ph.D. thesis, Stanford, CA, USA"},{"key":"278_CR4","doi-asserted-by":"crossref","unstructured":"Bobot F, Conchon S, Contejean E, Iguernelala M, Mahboubi A, Mebsout A, Melquiond G (2012) A simplex-based extension of Fourier\u2013Motzkin for solving linear integer arithmetic. In: IJCAR 2012, LNCS, vol 7364, pp 67\u201381","DOI":"10.1007\/978-3-642-31365-3_8"},{"key":"278_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex optimization","author":"S Boyd","year":"2004","unstructured":"Boyd S, Vandenberghe L (2004) Convex optimization. Cambridge University Press, Cambridge"},{"key":"278_CR6","doi-asserted-by":"crossref","unstructured":"Bromberger M, Sturm T, Weidenbach C (2015) Linear integer arithmetic revisited. In: CADE-25, LNCS, vol 9195, pp 623\u2013637","DOI":"10.1007\/978-3-319-21401-6_42"},{"key":"278_CR7","unstructured":"Bromberger M, Weidenbach C (2016) Computing a complete basis for equalities implied by a system of LRA constraints. In: SMT 2016, pp 15\u201330"},{"key":"278_CR8","doi-asserted-by":"crossref","unstructured":"Bromberger M, Weidenbach C (2016) Fast cube tests for lia constraint solving. In: IJCAR 2016, LNCS, vol 9706","DOI":"10.1007\/978-3-319-40229-1_9"},{"issue":"1","key":"278_CR9","first-page":"63","volume":"55","author":"R Bruttomesso","year":"2009","unstructured":"Bruttomesso R, Cimatti A, Franzen A, Griggio A, Sebastiani R (2009) Delayed theory combination vs. Nelson\u2013Oppen for satisfiability modulo theories: a comparative analysis. AMAI 55(1):63\u201399","journal-title":"AMAI"},{"key":"278_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT Solver. In: TACAS, LNCS, vol 7795","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"278_CR11","doi-asserted-by":"crossref","unstructured":"Dillig I, Dillig T, Aiken A (2009) Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. In: CAV, LNCS, vol 5643, pp 233\u2013247","DOI":"10.1007\/978-3-642-02658-4_20"},{"key":"278_CR12","doi-asserted-by":"crossref","unstructured":"Dolzmann A, Sturm T, Weispfenning V (1999) Real quantifier elimination in practice. In: Algorithmic algebra and number theory. Springer, pp 221\u2013247","DOI":"10.1007\/978-3-642-59932-3_11"},{"key":"278_CR13","unstructured":"Dutertre B (2014) Yices 2.2. In: CAV 2014, LNCS, vol 8559"},{"key":"278_CR14","doi-asserted-by":"crossref","unstructured":"Dutertre B, de Moura, L (2006) A fast linear-arithmetic solver for DPLL(T). In: CAV, LNCS, vol. 4144, pp. 81\u201394 (2006). Extended version: Integrating simplex with DPLL(T). Technical report, CSL, SRI International","DOI":"10.1007\/11817963_11"},{"key":"278_CR15","doi-asserted-by":"crossref","unstructured":"Faure G, Nieuwenhuis R, Oliveras A, Rodr\u00edguez-Carbonell E (2008) Sat modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: SAT 2008, LNCS, vol 4996, pp 77\u201390","DOI":"10.1007\/978-3-540-79719-7_8"},{"issue":"1\/2","key":"278_CR16","first-page":"1","volume":"8","author":"A Griggio","year":"2012","unstructured":"Griggio A (2012) A practical approach to satisfiability modulo linear integer arithmetic. JSAT 8(1\/2):1\u201327","journal-title":"JSAT"},{"issue":"4","key":"278_CR17","doi-asserted-by":"crossref","first-page":"600","DOI":"10.1287\/opre.17.4.600","volume":"17","author":"FS Hillier","year":"1969","unstructured":"Hillier FS (1969) Efficient heuristic procedures for integer linear programming with an interior. Oper Res 17(4):600\u2013637","journal-title":"Oper Res"},{"issue":"1","key":"278_CR18","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 (2013) Cutting to the chase. JAR 51(1):79\u2013108","journal-title":"JAR"},{"key":"278_CR19","doi-asserted-by":"crossref","unstructured":"J\u00fcnger M, Liebling TM, Naddef D, Nemhauser GL, Pulleyblank WR, Reinelt G, Rinaldi G, Wolsey LA (eds) (2010) 50 years of integer programming 1958\u20132008","DOI":"10.1007\/978-3-540-68279-0"},{"key":"278_CR20","doi-asserted-by":"crossref","unstructured":"Kannan R, Lov\u00e1sz L (1986) Covering minima and lattice point free convex bodies. FSTTCS, LNCS, vol 241, pp 193\u2013213","DOI":"10.1007\/3-540-17179-7_12"},{"issue":"4","key":"278_CR21","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF02579150","volume":"4","author":"N Karmarkar","year":"1984","unstructured":"Karmarkar N (1984) A new polynomial-time algorithm for linear programming. Combinatorica 4(4):373\u2013396","journal-title":"Combinatorica"},{"issue":"1","key":"278_CR22","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1002\/nav.3800010107","volume":"1","author":"CE Lemke","year":"1954","unstructured":"Lemke CE (1954) The dual method of solving the linear programming problem. Nav Res Logist Quart 1(1):36\u201347","journal-title":"Nav Res Logist Quart"},{"issue":"5","key":"278_CR23","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos R, Weispfenning V (1993) Applying linear quantifier elimination. Comput J 36(5):450\u2013462","journal-title":"Comput J"},{"key":"278_CR24","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems, LNCS, vol 4963, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"4","key":"278_CR25","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"CH Papadimitriou","year":"1981","unstructured":"Papadimitriou CH (1981) On the complexity of integer programming. J ACM 28(4):765\u2013768","journal-title":"J ACM"},{"key":"278_CR26","doi-asserted-by":"crossref","unstructured":"Pugh W (1991) The omega test: a fast and practical integer programming algorithm for dependence analysis. In: Supercomputing 1991, Supercomputing \u201991. ACM, pp 4\u201313","DOI":"10.1145\/125826.125848"},{"key":"278_CR27","doi-asserted-by":"crossref","unstructured":"Refalo P (1998) Approaches to the incremental detection of implicit equalities with the revised simplex method. In: PLILP 1998, LNCS, vol 1490, pp 481\u2013496","DOI":"10.1007\/BFb0056634"},{"key":"278_CR28","unstructured":"Rue\u00df H, Shankar N (2004) Solving linear arithmetic constraints. Technical report, SRI International, Computer Science Laboratory"},{"key":"278_CR29","volume-title":"Theory of linear and integer programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver A (1986) Theory of linear and integer programming. Wiley, New York"},{"key":"278_CR30","unstructured":"Sturm T (1996) Real quadratic quantifier elimination in risa\/asir. Technical report, ISIS-RM-5E, Fujitsu Laboratories Ltd"},{"issue":"10","key":"278_CR31","doi-asserted-by":"crossref","first-page":"1209","DOI":"10.1287\/mnsc.29.10.1209","volume":"29","author":"J Telgen","year":"1983","unstructured":"Telgen J (1983) Identifying redundant constraints and implicit equalities in systems of linear constraints. Manag Sci 29(10):1209\u20131222","journal-title":"Manag Sci"},{"issue":"2","key":"278_CR32","first-page":"303","volume":"5","author":"P Hentenryck Van","year":"1992","unstructured":"Van Hentenryck P, Graf T (1992) Standard forms for rational linear arithmetic in constraint logic programming. AMAI 5(2):303\u2013319","journal-title":"AMAI"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0278-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0278-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0278-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,23]],"date-time":"2019-09-23T16:24:02Z","timestamp":1569255842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0278-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,8]]},"references-count":32,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["278"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0278-7","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2017,5,8]]}}}