{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T11:17:07Z","timestamp":1790680627607,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642224379","type":"print"},{"value":"9783642224386","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_10","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"101-115","source":"Crossref","is-referenced-by-count":60,"title":["Blocked Clause Elimination for QBF"],"prefix":"10.1007","author":[{"given":"Armin","family":"Biere","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Lonsing","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-24605-3_26","volume-title":"Theory and Applications of Satisfiability Testing","author":"F. Bacchus","year":"2004","unstructured":"Bacchus, F., Winter, J.: Effective Preprocessing with Hyper-Resolution and Equality Reduction. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 341\u2013355. Springer, Heidelberg (2004)"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S1571-0653(04)00314-2","volume":"9","author":"D. Berre Le","year":"2001","unstructured":"Le Berre, D.: Exploiting the Real Power of Unit Propagation Lookahead. Electronic Notes in Discrete Mathematics\u00a09, 59\u201380 (2001)","journal-title":"Electronic Notes in Discrete Mathematics"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 59\u201370. Springer, Heidelberg (2005)"},{"key":"10_CR4","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.\u00a04501, pp. 244\u2013257. Springer, Heidelberg (2007)"},{"issue":"1","key":"10_CR5","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H.K. B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for Quantified Boolean Formulas. Information and Computation\u00a0117(1), 12\u201318 (1995)","journal-title":"Information and Computation"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 61\u201375. Springer, Heidelberg (2005)"},{"key":"10_CR7","first-page":"83","volume":"7","author":"E. Giunchiglia","year":"2010","unstructured":"Giunchiglia, E., Marin, P., Narizzano, M.: QuBE 7.0. JSAT\u00a07, 83\u201388 (2010)","journal-title":"JSAT"},{"key":"10_CR8","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":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-16242-8_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Heule","year":"2010","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for cnf formulas. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 357\u2013371. Springer, Heidelberg (2010)"},{"key":"#cr-split#-10_CR10.1","doi-asserted-by":"crossref","unstructured":"Heule, M., J\u00e4rvisalo, M., Biere, A.: Covered Clause Elimination. CoRR, abs\/1011.5202 (2010);","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"#cr-split#-10_CR10.2","unstructured":"Short paper proceedings LPAR-17"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked Clause Elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a Generalization of Extended Resolution. Discrete Applied Mathematics\u00a096, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-540-79719-7_19","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"F. Lonsing","year":"2008","unstructured":"Lonsing, F., Biere, A.: Nenofex: Expanding NNF for QBF solving. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 196\u2013210. Springer, Heidelberg (2008)"},{"key":"10_CR14","first-page":"71","volume":"7","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A Dependency-Aware QBF Solver (System Description). JSAT\u00a07, 71\u201376 (2010)","journal-title":"JSAT"},{"key":"10_CR15","first-page":"1695","volume-title":"Design, Automation and Test in Europe (DATE 2010)","author":"H. Mangassarian","year":"2010","unstructured":"Mangassarian, H., Le, B., Goultiaeva, A., Veneris, A.G., Bacchus, F.: Leveraging Dominators for Preprocessing QBF. In: Design, Automation and Test in Europe (DATE 2010), pp. 1695\u20131700. IEEE, Los Alamitos (2010)"},{"key":"10_CR16","first-page":"199","volume-title":"Proc. of the 8th Int. Conf. on Princ. and Pract. of Constraint Prog. (CP 2002)","author":"R. Ostrowski","year":"2006","unstructured":"Ostrowski, R., Grgoire, E., Mazure, B., Sa\u00efs, L.: Recovering and Exploiting Structural Knowledge from CNF Formulas. In: Proc. of the 8th Int. Conf. on Princ. and Pract. of Constraint Prog (CP 2002), pp. 199\u2013206. Springer, Heidelberg (2006)"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Scholl, C.: An AIG-Based QBF-Solver Using SAT for Preprocessing. In: Proc. of the 47th Design Aut. Conf (DAC 2010), pp. 170\u2013175 (2010)","DOI":"10.1145\/1837274.1837318"},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A Structure-Preserving Clause Form Translation. Journal of Symbolic Computation\u00a02(3), 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR19","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.\u00a04204, pp. 514\u2013529. Springer, Heidelberg (2006)"},{"issue":"115-125","key":"10_CR20","first-page":"10","volume":"2","author":"G.S. Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the Complexity of Derivation in Propositional Calculus. Studies in Constructive Mathematics and Mathematical Logic\u00a02(115-125), 10\u201313 (1968)","journal-title":"Studies in Constructive Mathematics and Mathematical Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,12]],"date-time":"2019-06-12T23:19:32Z","timestamp":1560381572000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}