{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T19:46:04Z","timestamp":1725479164688},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540262763"},{"type":"electronic","value":"9783540316794"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11499107_7","type":"book-chapter","created":{"date-parts":[[2010,7,14]],"date-time":"2010-07-14T21:56:25Z","timestamp":1279144585000},"page":"91-106","source":"Crossref","is-referenced-by-count":0,"title":["Local and Global Complete Solution Learning Methods for QBF"],"prefix":"10.1007","author":[{"given":"Ian P.","family":"Gent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew G. D.","family":"Rowley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H. Kleine Buning","year":"1995","unstructured":"Kleine Buning, H., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified boolean formulas. Information and Computation\u00a0117, 12\u201318 (1995)","journal-title":"Information and Computation"},{"issue":"2","key":"7_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., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning\u00a028(2), 101\u2013142 (2002)","journal-title":"Journal of Automated Reasoning"},{"issue":"7","key":"7_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., Loveland, D.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"7_CR4","unstructured":"Gent, I., Rowley, A.: Solution learning and solution directed backjumping revisited. Technical Report APES-80-2004, APES Research Group (2004), \n                    \n                      http:\/\/www.dcs.st-and.ac.uk\/~apes\/apesreports.html"},{"key":"7_CR5","first-page":"649","volume-title":"Proc. AAAI 2002","author":"E. Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Learning for quantified Boolean logic satisfiability. In: Proc. AAAI 2002, pp. 649\u2013654. AAAI Press, Menlo Park (2002)"},{"issue":"1\u20132","key":"7_CR6","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(02)00373-9","volume":"145","author":"E. Giunchiglia","year":"2003","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Backjumping for quantified boolean logic satisfiability. Artificial Intelligence\u00a0145(1\u20132), 99\u2013120 (2003)","journal-title":"Artificial Intelligence"},{"key":"7_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"issue":"3","key":"7_CR8","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1111\/j.1467-8640.1993.tb00310.x","volume":"9","author":"P. Prosser","year":"1993","unstructured":"Prosser, P.: Hybrid algorithms for the constraint satisfaction problem. Computational Intelligence\u00a09(3), 268\u2013299 (1993)","journal-title":"Computational Intelligence"},{"key":"7_CR9","first-page":"442","volume-title":"Proceedings of the 2002 IEEE\/ACM international conference on Computer-aided design","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: Proceedings of the 2002 IEEE\/ACM international conference on Computer-aided design, pp. 442\u2013449. ACM Press, New York (2002)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-44594-3","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"L. Zhang","year":"2000","unstructured":"Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 200\u2013215. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11499107_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:41:22Z","timestamp":1619505682000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11499107_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540262763","9783540316794"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/11499107_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}