{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:18:50Z","timestamp":1725740330575},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_44","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T19:13:06Z","timestamp":1373483586000},"page":"662-677","source":"Crossref","is-referenced-by-count":11,"title":["ILP Modulo Theories"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Vasilis","family":"Papavasileiou","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"44_CR1","unstructured":"CPLEX, \n                    \n                      http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/"},{"key":"44_CR2","unstructured":"Achterberg, T.: Constraint Integer Programming. PhD thesis, Technische Universitat Berlin (2007)"},{"key":"44_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 236\u2013249. Springer, Heidelberg (2002)"},{"issue":"1","key":"44_CR4","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1287\/opre.35.1.140","volume":"35","author":"R.H. Byrd","year":"1987","unstructured":"Byrd, R.H., Goldman, A.J., Heller, M.: Recognizing Unbounded Integer Programs. Operations Research\u00a035(1), 140\u2013142 (1987)","journal-title":"Operations Research"},{"key":"44_CR5","unstructured":"Papadimitriou, C., Steiglitz, K.: Combinatorial Optimization: Algorithms and Complexity, 2nd edn. Dover (1998)"},{"key":"44_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability Modulo the Theory of Costs: Foundations and Applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 99\u2013113. Springer, Heidelberg (2010)"},{"key":"44_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-20807-2_9","volume-title":"Integer Programming and Combinatoral Optimization","author":"W. Cook","year":"2011","unstructured":"Cook, W., Koch, T., Steffy, D.E., Wolter, K.: An Exact Rational Mixed-Integer Programming Solver. In: G\u00fcnl\u00fck, O., Woeginger, G.J. (eds.) IPCO 2011. LNCS, vol.\u00a06655, pp. 104\u2013116. Springer, Heidelberg (2011)"},{"key":"44_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"44_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Moura de","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A Model-Constructing Satisfiability Calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol.\u00a07737, pp. 1\u201312. Springer, Heidelberg (2013)"},{"key":"44_CR10","unstructured":"de Moura, L., Ruess, H.: Lemmas on Demand for Satisfiability Solvers. In: SAT (2002)"},{"key":"44_CR11","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":"44_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a04996, pp. 77\u201390. Springer, Heidelberg (2008)"},{"key":"44_CR13","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1090\/S0002-9904-1958-10224-4","volume":"64","author":"R.E. Gomory","year":"1958","unstructured":"Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bulletin of the AMS\u00a064, 275\u2013278 (1958)","journal-title":"Bulletin of the AMS"},{"key":"44_CR14","first-page":"1","volume":"8","author":"A. Griggio","year":"2012","unstructured":"Griggio, A.: A Practical Approach to Satisfiability Modulo Linear Integer Arithmetic. JSAT\u00a08, 1\u201327 (2012)","journal-title":"JSAT"},{"key":"44_CR15","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/BF01586932","volume":"51","author":"M. Grotschel","year":"1991","unstructured":"Grotschel, M., Holland, O.: Solution of large-scale symmetric travelling salesman problems. Mathematical Programming\u00a051, 141\u2013202 (1991)","journal-title":"Mathematical Programming"},{"key":"44_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-22110-1_35","volume-title":"Computer Aided Verification","author":"C. Hang","year":"2011","unstructured":"Hang, C., Manolios, P., Papavasileiou, V.: Synthesizing Cyber-Physical Architectural Models with Real-Time Constraints. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 441\u2013456. Springer, Heidelberg (2011)"},{"key":"44_CR17","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":"44_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/978-3-642-02658-4_35","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2009","unstructured":"McMillan, K.L., Kuehlmann, A., Sagiv, M.: Generalizing DPLL to Richer Logics. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 462\u2013476. Springer, Heidelberg (2009)"},{"key":"44_CR19","unstructured":"Manna, Z., Zarba, C.: Combining Decision Procedures. In: 10th Anniversary Colloquium of UNU\/IIST (2002)"},{"key":"44_CR20","doi-asserted-by":"crossref","unstructured":"Manolios, P., Papavasileiou, V.: ILP Modulo Theories. CoRR, abs\/1210.3761 (2012)","DOI":"10.1007\/978-3-642-39799-8_44"},{"key":"44_CR21","unstructured":"McCarthy, J.: Towards a Mathematical Science of Computation. In: Congress IFIP-1962 (1962)"},{"key":"44_CR22","unstructured":"Mitchell, J.E.: Branch-and-Cut Algorithms for Combinatorial Optimization Problems. In: Handbook of Applied Optimization, pp. 223\u2013233. Oxford University Press (2000)"},{"key":"44_CR23","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. TOPLAS\u00a01, 245\u2013257 (1979)","journal-title":"TOPLAS"},{"key":"44_CR24","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s10107-003-0433-3","volume":"99","author":"A. Neumaier","year":"2004","unstructured":"Neumaier, A., Shcherbina, O.: Safe bounds in linear and mixed-integer linear programming. Mathematical Programming\u00a099, 283\u2013296 (2004)","journal-title":"Mathematical Programming"},{"key":"44_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44881-0","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence Closure with Integer Offsets. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, Springer, Heidelberg (2003)"},{"key":"44_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11814948_18","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A.: On SAT Modulo Theories and Optimization Problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol.\u00a04121, pp. 156\u2013169. Springer, Heidelberg (2006)"},{"issue":"6","key":"44_CR27","doi-asserted-by":"publisher","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). JACM\u00a053(6), 937\u2013977 (2006)","journal-title":"JACM"},{"key":"44_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-642-15297-9_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Cotton","year":"2010","unstructured":"Cotton, S.: Natural domain SMT: A preliminary assessment. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol.\u00a06246, pp. 77\u201391. Springer, Heidelberg (2010)"},{"key":"44_CR29","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Tomasi, S.: Optimization in SMT with LA(Q) Cost Functions. In: IJCAR (2012)","DOI":"10.1007\/978-3-642-31365-3_38"},{"key":"44_CR30","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. In: LICS (2004)","DOI":"10.21236\/ADA461078"},{"key":"44_CR31","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.: A New Correctness Proof of the Nelson-Oppen Combination Procedure. In: FroCoS (1996)","DOI":"10.1007\/978-94-009-0349-4_5"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T14:21:00Z","timestamp":1557930060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}