{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T11:59:54Z","timestamp":1792756794566,"version":"4.5.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642120015","type":"print"},{"value":"9783642120022","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12002-2_10","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T01:20:25Z","timestamp":1268011225000},"page":"129-144","source":"Crossref","is-referenced-by-count":80,"title":["Blocked Clause Elimination"],"prefix":"10.1007","author":[{"given":"Matti","family":"J\u00e4rvisalo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/11527695_15","volume-title":"Theory and Applications of Satisfiability Testing","author":"P. Jackson","year":"2005","unstructured":"Jackson, P., Sheridan, D.: Clause form conversions for Boolean circuits. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 183\u2013198. Springer, Heidelberg (2005)"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1145\/1146909.1147048","volume-title":"DAC 2006","author":"A. Mishchenko","year":"2006","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: DAC 2006, pp. 532\u2013535. ACM, New York (2006)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-72788-0_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"N. E\u00e9n","year":"2007","unstructured":"E\u00e9n, N., Mishchenko, A., S\u00f6rensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 272\u2013286. Springer, Heidelberg (2007)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-540-72788-0_3","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"P. Manolios","year":"2007","unstructured":"Manolios, P., Vroon, D.: Efficient circuit to CNF conversion. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 4\u20139. Springer, Heidelberg (2007)"},{"key":"10_CR5","first-page":"1590","volume-title":"DATE 2009","author":"B. Chambers","year":"2009","unstructured":"Chambers, B., Manolios, P., Vroon, D.: Faster SAT solving with better CNF generation. In: DATE 2009, pp. 1590\u20131595. IEEE, Los Alamitos (2009)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-46135-3_13","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"R. Ostrowski","year":"2002","unstructured":"Ostrowski, R., Gr\u00e9goire, \u00c9., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 185\u2013199. Springer, Heidelberg (2002)"},{"issue":"1","key":"10_CR7","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/TSMCB.2002.805807","volume":"34","author":"R.I. Brafman","year":"2004","unstructured":"Brafman, R.I.: A simplifier for propositional formulas with many binary clauses. IEEE Transactions on Systems, Man, and Cybernetics, Part B\u00a034(1), 52\u201359 (2004)","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part B"},{"key":"10_CR8","first-page":"613","volume-title":"AAAI 2002","author":"F. Bacchus","year":"2002","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: AAAI 2002, pp. 613\u2013619. AAAI Press, Menlo Park (2002)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/11527695_22","volume-title":"Theory and Applications of Satisfiability Testing","author":"S. Subbarayan","year":"2005","unstructured":"Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 276\u2013291. Springer, Heidelberg (2005)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/11499107_34","volume-title":"Theory and Applications of Satisfiability Testing","author":"R. Gershman","year":"2005","unstructured":"Gershman, R., Strichman, O.: Cost-effective hyper-resolution for preprocessing CNF formulas. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 423\u2013429. Springer, Heidelberg (2005)"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96-97","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics\u00a096-97, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"key":"10_CR13","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970","author":"G.S. Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967\u20131970, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"issue":"3","key":"10_CR14","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_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-48683-6_8","volume-title":"Computer Aided Verification","author":"A. Biere","year":"1999","unstructured":"Biere, A., Clarke, E.M., Raimi, R., Zhu, Y.: Verifiying safety properties of a power PC microprocessor using symbolic model checking without BDDs. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 60\u201371. Springer, Heidelberg (1999)"},{"issue":"3","key":"10_CR16","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/j.entcs.2006.12.022","volume":"174","author":"T. Jussila","year":"2007","unstructured":"Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electronic Notes in Theoretical Computer Science\u00a0174(3), 45\u201356 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10_CR17","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"655","volume-title":"Handbook of Satisfiability","author":"R. Drechsler","year":"2009","unstructured":"Drechsler, R., Junttila, T., Niemel\u00e4, I.: Non-clausal SAT and ATPG. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 655\u2013694. IOS Press, Amsterdam (2009)"},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"4","key":"10_CR19","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1109\/TPAMI.1984.4767555","volume":"6","author":"P.W. Purdom","year":"1984","unstructured":"Purdom, P.W.: Solving satisfiability with less searching. IEEE Transactions on Pattern Analysis and Machine Intelligence\u00a06(4), 510\u2013513 (1984)","journal-title":"IEEE Transactions on Pattern Analysis and Machine Intelligence"},{"key":"10_CR20","first-page":"351","volume-title":"IJCAI 2001","author":"H.A. Kautz","year":"2001","unstructured":"Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and filtering in structured satisfiable problems. In: IJCAI 2001, pp. 351\u2013358. Morgan Kaufmann, San Francisco (2001)"},{"key":"10_CR21","unstructured":"Heule, M.J.H., Verwer, S.: Using a satisfiability solver to identify deterministic finite state automata. In: BNAIC 2009, pp. 91\u201398 (2009)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"TACAS 2009","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12002-2_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:17Z","timestamp":1606185977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12002-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120015","9783642120022"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12002-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}