{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:32:50Z","timestamp":1725471170166},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_39","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"468-482","source":"Crossref","is-referenced-by-count":1,"title":["Solving Sparse Linear Constraints"],"prefix":"10.1007","author":[{"given":"Shuvendu K.","family":"Lahiri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Madanlal","family":"Musuvathi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"39_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11591191_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T. Ball","year":"2005","unstructured":"Ball, T., Lahiri, S.K., Musuvathi, M.: Zap: Automated theorem proving for software analysis. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 2\u201322. Springer, Heidelberg (2005)"},{"key":"39_CR2","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":"39_CR3","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1090\/qam\/102435","volume":"16","author":"R. Bellman","year":"1958","unstructured":"Bellman, R.: On a routing problem. Quarterly of Applied Mathematics\u00a016(1), 87\u201390 (1958)","journal-title":"Quarterly of Applied Mathematics"},{"key":"39_CR4","doi-asserted-by":"crossref","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-cycle detection algorithms. In: European Symposium on Algorithms, pp. 349\u2013363 (1996)","DOI":"10.1007\/3-540-61680-2_67"},{"key":"39_CR5","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"key":"39_CR6","volume-title":"Linear programming and extensions","author":"G. Dantzig","year":"1963","unstructured":"Dantzig, G.: Linear programming and extensions. Princeton University Press, Princeton (1963)"},{"key":"39_CR7","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical report, HPL-2003-148 (2003)"},{"key":"39_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.: Theorem proving using lazy proof explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"39_CR9","doi-asserted-by":"crossref","unstructured":"Ford Jr., L.R., Fulkerson, D.R.: Flows in Networks (1962)","DOI":"10.1515\/9781400875184"},{"key":"39_CR10","unstructured":"Harvey, W., Stuckey, P.J.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proceedings of the 20th Australasian Computer Science Conference (ACSC 1997), pp. 102\u2013111 (1997)"},{"key":"39_CR11","unstructured":"ILOG CPLEX, Available at http:\/\/ilog.com\/products\/cplex"},{"key":"39_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/3-540-58601-6_92","volume-title":"Principles and Practice of Constraint Programming","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.J., Stuckey, P.J., Yap, H.C.: Beyond finite domains. In: Borning, A. (ed.) PPCP 1994. LNCS, vol.\u00a0874, pp. 86\u201394. Springer, Heidelberg (1994)"},{"issue":"4","key":"39_CR13","doi-asserted-by":"publisher","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\u00a04(4), 373\u2013396 (1984)","journal-title":"Combinatorica"},{"key":"39_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/11559306_9","volume-title":"Frontiers of Combining Systems","author":"S.K. Lahiri","year":"2005","unstructured":"Lahiri, S.K., Musuvathi, M.: An efficient decision procedure for UTVPI constraints. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 168\u2013183. Springer, Heidelberg (2005)"},{"key":"39_CR15","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Musuvathi, M.: An Efficient Nelson-Oppen Decision Procedure for Difference Constraints over Rationals. In: Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005). ENTCS, vol.\u00a0144, pp. 27\u201341 (2005)","DOI":"10.1016\/j.entcs.2005.12.004"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Musuvathi, M.: Solving sparse linear constraints. Technical Report MSR-TR-2006-47, Microsoft Research (2006)","DOI":"10.1007\/11814771_39"},{"key":"39_CR17","unstructured":"LP_SOLVE: available at http:\/\/groups.yahoo.com\/group\/lp_solve\/"},{"key":"39_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10721959_3","volume-title":"Automated Deduction - CADE-17","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C., Lee, P.: Proof generation in the touchstone theorem prover. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 25\u201344. Springer, Heidelberg (2000)"},{"issue":"1","key":"39_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"2","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a02(1), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"issue":"4","key":"39_CR20","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C.H. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM\u00a028(4), 765\u2013768 (1981)","journal-title":"J. ACM"},{"key":"39_CR21","unstructured":"Pratt, V.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology, Cambridge, Mass (September 1977)"},{"key":"39_CR22","unstructured":"Rue\u00df, H., Shankar, N.: Solving linear arithmetic constraints. Technical Report CSL-SRI-04-01, SRI International (January 2004)"},{"key":"39_CR23","volume-title":"Theory of Linear and Integer Programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)"},{"key":"39_CR24","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding quantifier-free Presburger formulas using parameterized solution bounds. In: LICS 2004: Logic in Computer Science, pp. 100\u2013109 (July 2004)","DOI":"10.1109\/LICS.2004.1319604"},{"key":"39_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/11499107_18","volume-title":"Theory and Applications of Satisfiability Testing","author":"H.M. Sheini","year":"2005","unstructured":"Sheini, H.M., Sakallah, K.A.: A scalable method for solving satisfiability of integer linear arithmetic logic. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 241\u2013256. Springer, Heidelberg (2005)"},{"key":"39_CR26","unstructured":"SMT-LIB: The Satisfiability Modulo Theories Library, available at http:\/\/combination.cs.uiowa.edu\/smtlib\/"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:14:36Z","timestamp":1605626076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11814771_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}