{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T04:41:59Z","timestamp":1777092119239,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642316111","type":"print"},{"value":"9783642316128","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31612-8_8","type":"book-chapter","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T05:14:42Z","timestamp":1339996482000},"page":"86-99","source":"Crossref","is-referenced-by-count":4,"title":["Extended Failed-Literal Preprocessing for Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Allen","family":"Van Gelder","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samuel B.","family":"Wood","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked Clause Elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"key":"8_CR2","unstructured":"Freeman, J.W.: Failed literals in the Davis-Putnam procedure for SAT. In: DIMACS Challenge Workshop: Cliques, Coloring and Satisfiability (1993)"},{"key":"8_CR3","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.\u00a06175, pp. 85\u201398. Springer, Heidelberg (2010)"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-540-30201-8_21","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2004","author":"E. Giunchiglia","year":"2004","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: Monotone Literals and Learning in QBF Reasoning. In: Wallace, M. (ed.) CP 2004. LNCS, vol.\u00a03258, pp. 260\u2013273. Springer, Heidelberg (2004)"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/A:1006366304347","volume":"24","author":"J.F. Groote","year":"2000","unstructured":"Groote, J.F., Warners, J.P.: The propositional formula checker HeerHugo. J. Automated Reasoning\u00a024(1), 101\u2013125 (2000)","journal-title":"J. Automated Reasoning"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"T. Jussila","year":"2007","unstructured":"Jussila, T., Biere, A., Sinz, C., Kroning, D., Wintersteiger, C.M.: A First Step Towards a Unified Proof Checker for QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 201\u2013214. Springer, Heidelberg (2007)"},{"key":"8_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., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified boolean formulas. Information and Computation\u00a0117, 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"8_CR8","unstructured":"Kleine B\u00fcning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press (1999)"},{"key":"8_CR9","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.\u00a06175, pp. 128\u2013142. Springer, Heidelberg (2010)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Le Berre, D.: Exploiting the real power of unit propagation lookahead. In: IEEE\/ASL LICS Satisfiability Workshop, pp. 59\u201380. Elsevier (2001)","DOI":"10.1016\/S1571-0653(04)00314-2"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-642-21581-0_21","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"F. Lonsing","year":"2011","unstructured":"Lonsing, F., Biere, A.: Failed Literal Detection for QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 259\u2013272. Springer, Heidelberg (2011)"},{"key":"8_CR12","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.\u00a04501, pp. 215\u2013229. Springer, Heidelberg (2007)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-21581-0_25","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"A. Van Gelder","year":"2011","unstructured":"Van Gelder, A.: Careful Ranking of Multiple Solvers with Timeouts and Ties. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 317\u2013328. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2014 SAT 2012"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31612-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T04:08:46Z","timestamp":1777090126000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31612-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316111","9783642316128"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31612-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}