{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:36Z","timestamp":1725542976649},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372066"},{"type":"electronic","value":"9783540372073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_17","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T10:12:38Z","timestamp":1153217558000},"page":"142-155","source":"Crossref","is-referenced-by-count":6,"title":["Lemma Learning in SMT on Linear Constraints"],"prefix":"10.1007","author":[{"given":"Yinlei","family":"Yu","sequence":"first","affiliation":[]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Sofware Design Group, MIT: The Alloy Analyzer (2006) Retrieved on (May 12, 2006), http:\/\/alloy.mit.edu\/"},{"issue":"3","key":"17_CR2","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"Journal of the ACM"},{"issue":"5","key":"17_CR3","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP - a search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. DAC, pp. 530\u2013535.","DOI":"10.1145\/378239.379017"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: Proc. ICCAD (2001)","DOI":"10.1145\/774572.774637"},{"issue":"3","key":"17_CR6","doi-asserted-by":"publisher","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. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"7","key":"17_CR7","doi-asserted-by":"publisher","first-page":"394","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. Communications of the ACM\u00a05(7), 394 (1962)","journal-title":"Communications of the ACM"},{"key":"17_CR8","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. ACM Transactions on Programming Languages and Systems\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Borning, A., Marriott, K., Stuckey, P., Xiao, Y.: Solving linear arithmetic constraints for user interface applications. In: Proc. ACM Symp. on User Interface Software and Technology, pp. 87\u201396 (1996)","DOI":"10.1145\/263407.263518"},{"key":"17_CR10","unstructured":"ILog, S.A.: CPLEX Manual, Version 10.0 (2006)"},{"key":"17_CR11","unstructured":"Dash optimization Inc.: Xpress-MP optimization software (2006), http:\/\/www.dashoptimization.com\/"},{"key":"17_CR12","unstructured":"Mosek ApS: MOSEK optimization software (2006), http:\/\/www.mosek.com\/"},{"key":"17_CR13","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":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and layered procedure for the satisfiability of linear arithmetic logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2002","unstructured":"Barrett, C., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation into SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/11513988_33","volume-title":"Computer Aided Verification","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 321\u2013334. Springer, Heidelberg (2005)"},{"key":"17_CR17","unstructured":"Rue\u00df, H., Shankar, N.: Solving linear arithmetic constraints. Technical report, SRI International (2004)"},{"issue":"1","key":"17_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0305-0548(94)90057-4","volume":"21","author":"J.W. Chinneck","year":"1994","unstructured":"Chinneck, J.W.: MINOS(IIS): Infeasibility analysis using MINOS. Computers and Operations Research\u00a021(1), 1\u20139 (1994)","journal-title":"Computers and Operations Research"},{"issue":"1","key":"17_CR19","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1287\/ijoc.11.1.63","volume":"11","author":"O. Guieu","year":"1999","unstructured":"Guieu, O., Chinneck, J.W.: Analyzing infeasible mixed-integer and integer linear programs. INFORMS J. of Computing\u00a011(1), 63\u201377 (1999)","journal-title":"INFORMS J. of Computing"},{"key":"17_CR20","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB standard: Version 1.1 (2005), http:\/\/combination.cs.uiowa.edu\/smtlib\/papers\/format-v1.1r05.04.12.pdf"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Bor\u00e4lv, A.: DAG-aware circuit compression for formal verification. In: Proc. ICCAD, pp. 42\u201349 (2004)","DOI":"10.1109\/ICCAD.2004.1382541"},{"key":"17_CR22","unstructured":"Dutertre, B., de Moura, L.: Simplics: Tool description (2005) retrieved on May 12, 2006, http:\/\/fm.csl.sri.com\/simplics\/description.pdf"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 20\u201323. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:27:54Z","timestamp":1619508474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11814948_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}