{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T15:05:46Z","timestamp":1725635146796},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_26","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T08:51:59Z","timestamp":1286182319000},"page":"357-371","source":"Crossref","is-referenced-by-count":31,"title":["Clause Elimination Procedures for CNF Formulas"],"prefix":"10.1007","author":[{"given":"Marijn","family":"Heule","sequence":"first","affiliation":[]},{"given":"Matti","family":"J\u00e4rvisalo","sequence":"additional","affiliation":[]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Freeman, J.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania (1995)"},{"key":"26_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":"26_CR3","unstructured":"Lynce, I., Marques-Silva, J.: The interaction between simplification and search in propositional satisfiability. In: CP 2001 Workshop on Modeling and Problem Formulation (2001)"},{"key":"26_CR4","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":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"26_CR6","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":"26_CR7","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)"},{"issue":"1","key":"26_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10472-005-0433-5","volume":"43","author":"A.V. Gelder","year":"2005","unstructured":"Gelder, A.V.: 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"},{"issue":"2","key":"26_CR9","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.entcs.2004.06.062","volume":"119","author":"H. Jin","year":"2005","unstructured":"Jin, H., Somenzi, F.: An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science\u00a0119(2), 51\u201365 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"26_CR10","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":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"TACAS 2010","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":"26_CR12","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O. Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics\u00a096\u201397, 149\u2013176 (1999)","journal-title":"Discrete Applied Mathematics"},{"issue":"2","key":"26_CR13","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":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-14186-7_30","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"M. J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A.: Reconstructing solutions after blocked clause elimination. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2010. LNCS, vol.\u00a06175, pp. 340\u2013345. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T10:10:21Z","timestamp":1553163021000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}