{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:02:25Z","timestamp":1777125745390,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642215803","type":"print"},{"value":"9783642215810","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-21581-0_17","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:30:19Z","timestamp":1307698219000},"page":"201-215","source":"Crossref","is-referenced-by-count":29,"title":["Efficient CNF Simplification Based on Binary Implication Graphs"],"prefix":"10.1007","author":[{"given":"Marijn J. H.","family":"Heule","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","first-page":"613","volume-title":"Proc.\u00a0AAAI","author":"F. Bacchus","year":"2002","unstructured":"Bacchus, F.: Enhancing Davis Putnam with extended binary clause reasoning. In: Proc.\u00a0AAAI, pp. 613\u2013619. AAAI Press, Menlo Park (2002)"},{"key":"17_CR2","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":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"17_CR4","first-page":"582","volume-title":"Proc.\u00a0DAC","author":"H. Han","year":"2007","unstructured":"Han, H., Somenzi, F.: Alembic: An efficient algorithm for CNF preprocessing. In: Proc.\u00a0DAC, pp. 582\u2013587. IEEE, Los Alamitos (2007)"},{"key":"17_CR5","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.J.H.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"17_CR6","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.J.H. 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.\u00a06397, pp. 357\u2013371. Springer, Heidelberg (2010)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-45349-0_45","volume-title":"Principles and Practice of Constraint Programming - CP 2000","author":"J.P. Marques-Silva","year":"2000","unstructured":"Marques-Silva, J.P.: Algebraic simplification techniques for propositional satisfiability. In: Dechter, R. (ed.) CP 2000. LNCS, vol.\u00a01894, pp. 537\u2013542. Springer, Heidelberg (2000)"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A. Gelder Van","year":"2005","unstructured":"Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Annals of Mathematics and Artificial Intelligence\u00a043(1), 239\u2013253 (2005)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"17_CR9","unstructured":"Li, C.M.: Integrating equivalency reasoning into Davis-Putnam procedure. In: Proc.\u00a0AAAI, pp. 291\u2013296 (2000)"},{"issue":"1","key":"17_CR10","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/TSMCB.2002.805807","volume":"34","author":"R. Brafman","year":"2004","unstructured":"Brafman, R.: 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"},{"issue":"2","key":"17_CR11","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1137\/0201008","volume":"1","author":"A. Aho","year":"1972","unstructured":"Aho, A., Garey, M., Ullman, J.: The transitive reduction of a directed graph. SIAM Journal on Computing\u00a01(2), 131\u2013137 (1972)","journal-title":"SIAM Journal on Computing"},{"key":"17_CR12","unstructured":"Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. FMV Report Series Technical Report 10\/1, Johannes Kepler University, Linz, Austria (2010)"},{"key":"17_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/3-540-45653-8_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"\u00c1. Val del","year":"2001","unstructured":"del Val, \u00c1.: Simplifying binary propositional theories into connected components twice as fast. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 392\u2013406. Springer, Heidelberg (2001)"},{"key":"17_CR14","unstructured":"Soos, M.: Cryptominisat 2.5.0, sat race 2010 solver description (2010)"},{"key":"17_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"issue":"1\/2","key":"17_CR16","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. Autom. Reasoning\u00a024(1\/2), 101\u2013125 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth-first search and linear graph algorithms. SIAM J. Computing 1(2) (1972)","DOI":"10.1137\/0201010"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,28]],"date-time":"2019-03-28T11:42:58Z","timestamp":1553773378000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}