{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T23:34:19Z","timestamp":1725838459533},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662488980"},{"type":"electronic","value":"9783662488997"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48899-7_29","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T03:59:28Z","timestamp":1448078368000},"page":"418-433","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination"],"prefix":"10.1007","author":[{"given":"Florian","family":"Lonsing","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fahiem","family":"Bacchus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Egly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"29_CR1","unstructured":"Ans\u00f3tegui, C., Gomes, C.P., Selman, B.: The achilles\u2019 heel of QBF. In: AAAI\/IAAI, pp. 275\u2013281. AAAI Press\/The MIT Press (2005)"},{"issue":"1\u20134","key":"29_CR2","first-page":"133","volume":"5","author":"M Benedetti","year":"2008","unstructured":"Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. JSAT 5(1\u20134), 133\u2013191 (2008)","journal-title":"JSAT"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-540-72788-0_24","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"U Bubeck","year":"2007","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Bounded universal expansion for preprocessing QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 244\u2013257. Springer, Heidelberg (2007)"},{"issue":"7","key":"29_CR4","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.W.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"1","key":"29_CR5","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/s10601-008-9055-y","volume":"14","author":"U Egly","year":"2009","unstructured":"Egly, U., Seidl, M., Woltran, S.: A solver for QBFs in negation normal form. Constraints 14(1), 38\u201379 (2009)","journal-title":"Constraints"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-24605-3_3","volume-title":"Theory and Applications of Satisfiability Testing","author":"IP Gent","year":"2004","unstructured":"Gent, I.P., Giunchiglia, E., Narizzano, M., Rowley, A.G.D., Tacchella, A.: Watched data structures for QBF solvers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 25\u201336. Springer, Heidelberg (2004)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-14186-7_9","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"E Giunchiglia","year":"2010","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 85\u201398. Springer, Heidelberg (2010)"},{"key":"29_CR8","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E Giunchiglia","year":"2006","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Clause\/term resolution and learning in the evaluation of quantified boolean formulas. JAIR 26, 371\u2013416 (2006)","journal-title":"JAIR"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-14186-7_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A Goultiaeva","year":"2010","unstructured":"Goultiaeva, A., Bacchus, F.: Exploiting circuit representations in QBF solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 333\u2013339. Springer, Heidelberg (2010)"},{"key":"29_CR10","doi-asserted-by":"crossref","unstructured":"Goultiaeva, A., Seidl, M., Biere, A.: Bridging the gap between dual propagation and CNF-based QBF solving. In: J\u00e4rvisalo, M., Van Gelder, A. (ed.) DATE, pp. 811\u2013814. ACM (2013)","DOI":"10.7873\/DATE.2013.172"},{"key":"29_CR11","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"M Heule","year":"2015","unstructured":"Heule, M., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. JAIR 53, 127\u2013168 (2015)","journal-title":"JAIR"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-642-45221-5_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M Janota","year":"2013","unstructured":"Janota, M., Grigore, R., Marques-Silva, J.: On QBF proofs and preprocessing. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 473\u2013489. Springer, Heidelberg (2013)"},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"issue":"1","key":"29_CR14","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., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-14186-7_12","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"W Klieber","year":"2010","unstructured":"Klieber, W., Sapra, S., Gao, S., Clarke, E.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science (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. 2381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"29_CR17","unstructured":"Pulina, L., Tacchella, A.: A structural approach to reasoning with quantified boolean formulas. In: IJCAI, pp. 596\u2013602 (2009)"},{"issue":"3","key":"29_CR18","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1023\/A:1005721905269","volume":"18","author":"A Ramesh","year":"1997","unstructured":"Ramesh, A., Becker, G., Murray, N.V.: CNF and DNF considered harmful for computing prime implicants\/implicates. JAIR 18(3), 337\u2013356 (1997)","journal-title":"JAIR"},{"issue":"1","key":"29_CR19","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","volume":"42","author":"M Samer","year":"2009","unstructured":"Samer, M., Szeider, S.: Backdoor sets of quantified boolean formulas. JAR 42(1), 77\u201397 (2009)","journal-title":"JAR"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-540-72788-0_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"H Samulowitz","year":"2007","unstructured":"Samulowitz, H., Bacchus, F.: Dynamically partitioning for solving QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 215\u2013229. Springer, Heidelberg (2007)"},{"key":"29_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/11889205_37","volume-title":"Principles and Practice of Constraint Programming - CP 2006","author":"H Samulowitz","year":"2006","unstructured":"Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) CP 2006. LNCS, vol. 4204, pp. 514\u2013529. Springer, Heidelberg (2006)"},{"issue":"2","key":"29_CR22","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0022-0000(78)90045-4","volume":"16","author":"TJ Schaefer","year":"1978","unstructured":"Schaefer, T.J.: On the complexity of some two-person perfect-information games. J. Comput. Syst. Sci. 16(2), 185\u2013225 (1978)","journal-title":"J. Comput. Syst. Sci."},{"issue":"5","key":"29_CR23","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JPM Silva","year":"1999","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"29_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/978-3-642-33558-7_47","volume-title":"Principles and Practice of Constraint Programming","author":"A Gelder Van","year":"2012","unstructured":"Van Gelder, A.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 647\u2013663. Springer, Heidelberg (2012)"},{"key":"29_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/978-3-642-40627-0_51","volume-title":"Principles and Practice of Constraint Programming","author":"A Gelder Van","year":"2013","unstructured":"Van Gelder, A.: Primal and dual encoding from applications into quantified boolean formulas. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 694\u2013707. Springer, Heidelberg (2013)"},{"key":"29_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-642-31612-8_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A Gelder Van","year":"2012","unstructured":"Van Gelder, A., Wood, S.B., Lonsing, F.: Extended failed-literal preprocessing for quantified boolean formulas. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 86\u201399. Springer, Heidelberg (2012)"},{"key":"29_CR27","unstructured":"Zhang, L.: Solving QBF by combining conjunctive and disjunctive normal forms. In: Dustdar, S., Schall, D., Skopik, F., Juszczyk, L., Psaier, H. (eds.) AAAI\/IAAI, pp. 143\u2013150. AAAI Press (2006)"},{"key":"29_CR28","doi-asserted-by":"crossref","unstructured":"Zhang, L., Malik, S.: Conflict driven learning in a quantified boolean satisfiability solver. In: ICCAD, pp. 442\u2013449. ACM\/IEEE Computer Society (2002)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48899-7_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T19:29:27Z","timestamp":1559330967000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48899-7_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662488980","9783662488997"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48899-7_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"22 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}