{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:29:22Z","timestamp":1725892162910},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_8","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T20:35:34Z","timestamp":1340310934000},"page":"67-81","source":"Crossref","is-referenced-by-count":11,"title":["A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Bobot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Conchon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evelyne","family":"Contejean","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed","family":"Iguernelala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Mebsout","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Melquiond","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"8_CR1","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1016\/j.orl.2005.07.009","volume":"34","author":"T. Achterberg","year":"2006","unstructured":"Achterberg, T., Koch, T., Martin, A.: MIPLIB 2003. Operations Research Letters\u00a034(4), 361\u2013372 (2006)","journal-title":"Operations Research Letters"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-6894-6","volume-title":"Dependence Analysis for Supercomputing","author":"U. Banerjee","year":"1988","unstructured":"Banerjee, U.: Dependence Analysis for Supercomputing. Kluwer Academic Publishers, Norwell (1988)"},{"key":"8_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on Demand in SAT Modulo Theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 512\u2013526. Springer, Heidelberg (2006)"},{"key":"8_CR4","unstructured":"Bobot, F., Conchon, S., Contejean, E., Iguernelala, M., Lescuyer, S., Mebsout, A.: The Alt-Ergo Automated Theorem Prover, http:\/\/alt-ergo.lri.fr"},{"key":"8_CR5","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3, an efficient SMT solver, http:\/\/research.microsoft.com\/projects\/z3"},{"key":"8_CR6","unstructured":"de Moura, L., Dutertre, B.: Yices: An SMT Solver, http:\/\/yices.csl.sri.com"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a05643, pp. 233\u2013247. Springer, Heidelberg (2009)"},{"key":"8_CR8","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_CR9","first-page":"1","volume":"124","author":"G. Farkas","year":"1902","unstructured":"Farkas, G.: \u00dcber die theorie der einfachen ungleichungen. Journal f\u00fcr die Reine und Angewandte Mathematik\u00a0124, 1\u201327 (1902)","journal-title":"Journal f\u00fcr die Reine und Angewandte Mathematik"},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/SAT190086","volume":"8","author":"A. Griggio","year":"2012","unstructured":"Griggio, A.: A practical approach to satisability modulo linear integer arithmetic. Journal on Satisfiability, Boolean Modeling and Computation\u00a08, 1\u201327 (2012)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"8_CR11","unstructured":"Griggio, A., Schaafsma, B., Cimatti, A., Sebastiani, R.: MathSAT 5: An SMT Solver for Formal Verification, http:\/\/mathsat.fbk.eu\/\/"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-22438-6_26","volume-title":"Automated Deduction \u2013 CADE-23","author":"D. Jovanovi\u0107","year":"2011","unstructured":"Jovanovi\u0107, D., de Moura, L.: Cutting to the Chase Solving Linear Integer Arithmetic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 338\u2013353. Springer, Heidelberg (2011)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-22438-6_28","volume-title":"Automated Deduction \u2013 CADE-23","author":"K. Korovin","year":"2011","unstructured":"Korovin, K., Voronkov, A.: Solving Systems of Linear Inequalities by Bound Propagation. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 369\u2013383. Springer, Heidelberg (2011)"},{"key":"8_CR14","unstructured":"Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer Publishing Company, Incorporated (2008)"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/125826.125848","volume-title":"Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing 1991","author":"W. Pugh","year":"1991","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing 1991, pp. 4\u201313. ACM, New York (1991)"},{"key":"8_CR16","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. John Wiley & Sons (1998)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:58:34Z","timestamp":1620129514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}