{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,25]],"date-time":"2026-06-25T15:15:34Z","timestamp":1782400534707,"version":"3.54.5"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319175232","type":"print"},{"value":"9783319175249","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17524-9_33","type":"book-chapter","created":{"date-parts":[[2015,4,7]],"date-time":"2015-04-07T06:15:31Z","timestamp":1428387331000},"page":"436-442","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Blocked Literals Are Universal"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,4,8]]},"reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/978-3-319-08587-6_7","volume-title":"Automated Reasoning","author":"MJH Heule","year":"2014","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 91\u2013106. Springer, Heidelberg (2014)"},{"key":"33_CR2","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, M., Giovanardi, M.: An algorithm to evaluate quantified boolean formulae and its experimental evaluation. Journal of Automated Reasoning, 262\u2013267 (1999)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 6803, pp. 101\u2013115. Springer, Heidelberg (2011)"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning 2, pp. 466\u2013483. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"33_CR5","unstructured":"Ans\u00f3tegui, C., Gomes, C.P., Selman, B.: The Achilles\u2019 Heel of QBF. In: AAAI 2005, pp. 275\u2013281. AAAI Press \/ The MIT Press (2005)"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: Efficient Extraction of Skolem Functions from QRAT Proofs. In: FMCAD 2014, pp. 107\u2013114. IEEE (2014)","DOI":"10.1109\/FMCAD.2014.6987602"},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/978-3-642-16242-8_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"MJH Heule","year":"2010","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357\u2013371. Springer, Heidelberg (2010)"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: LPAR-17-short. EPiC Series, vol. 13, pp. 41\u201346. EasyChair (2013)","DOI":"10.29007\/cl8s"},{"key":"33_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/11527695_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"A Biere","year":"2005","unstructured":"Biere, A.: Resolve and expand. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 59\u201370. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17524-9_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T23:26:19Z","timestamp":1747869979000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17524-9_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175232","9783319175249"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17524-9_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"8 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}