{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:45Z","timestamp":1761611205753,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439295"},{"type":"electronic","value":"9783540456162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_12","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:26:55Z","timestamp":1179376015000},"page":"160-175","source":"Crossref","is-referenced-by-count":73,"title":["Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Bayardo Jr., R.J. and Schrag, R.C. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings AAAI, pages 203\u2013208, 1997.","DOI":"10.1007\/3-540-61551-2_65"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M. Cadoli","year":"2002","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A. and Giovanardi, M. An Algorithm to Evaluate Quantified Boolean Formulae and its Evaluation. Journal of Automated Reasoning 28(2): 101\u2013142, 2002.","journal-title":"Journal of Automated Reasoning"},{"issue":"7","key":"12_CR3","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G. and Loveland, D.W. A Machine Program for Theorem Proving. Communications of the ACM, 5(7):394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"12_CR4","unstructured":"Feldmann, R., Monien, B. and Schamberger, S. A Distributed Algorithm to Evaluate Quantified Boolean Formulae. In Proceedings of AAAI, pages 285\u2013290, 2000."},{"key":"12_CR5","unstructured":"Giunchiglia, E., Narizzano, M. and Tacchella, A. Backjumping for quantified boolean logic satisfiability. In proceedings of IJCAI, pages 275\u2013281, 2001."},{"key":"12_CR6","unstructured":"Giunchiglia, E., Narizzano, M. and Tacchella, A. Learning for Quantified Boolean Logic Satisfiability In Proceedings AAAI, 2002."},{"issue":"1","key":"12_CR7","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine-B\u00fcning","year":"1995","unstructured":"Kleine-B\u00fcning, H., Karpinsky, M. and Fl\u00f6gel, A. Resolution for Quantified Boolean Formulas, Information and computation, 117(1):12\u201318, 1995.","journal-title":"Information and computation"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P. and Sakallah, K.A. GRASP \u2014 A New Search Algorithm for Satisfiability. In Proceedings of IEEE\/ACM International Conference on Computer-Aided Design, pages 220\u2013227, 1996.","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"12_CR9","unstructured":"Rintanen, J.T. Improvements to the Evaluation of Quantified Boolean Formulae. In Proceedings of IJCAI, pages 1192\u20131197, 1999."}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45616-3_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T11:07:28Z","timestamp":1737025648000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}