{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T18:09:48Z","timestamp":1776881388857,"version":"3.51.2"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319942049","type":"print"},{"value":"9783319942056","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94205-6_34","type":"book-chapter","created":{"date-parts":[[2018,6,29]],"date-time":"2018-06-29T16:22:50Z","timestamp":1530289370000},"page":"516-531","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Extended Resolution Simulates DRAT"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Kiesl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adri\u00e1n","family":"Rebola-Pardo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,30]]},"reference":[{"key":"34_CR1","series-title":"Trends in Logic","volume-title":"Methods of Cut-Elimination","author":"M Baaz","year":"2011","unstructured":"Baaz, M., Leitsch, A.: Methods of Cut-Elimination. Trends in Logic, vol. 3. Springer, Heidelberg (2011)"},{"key":"34_CR2","unstructured":"Biere, A.: Two pigeons per hole problem. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, p. 103 (2013)"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"Chatalic, P., Simon, L.: Multi-resolution on compressed sets of clauses. In: Proceedings of the 12th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2000), pp. 2\u201310 (2000)","DOI":"10.1109\/TAI.2000.889839"},{"issue":"4","key":"34_CR4","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/1008335.1008338","volume":"8","author":"SA Cook","year":"1976","unstructured":"Cook, S.A.: A short proof of the pigeon hole principle using extended resolution. SIGACT News 8(4), 28\u201332 (1976)","journal-title":"SIGACT News"},{"issue":"1","key":"34_CR5","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Log."},{"key":"34_CR6","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-89963-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MJH Heule","year":"2018","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 75\u201392. Springer, Cham (2018)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-319-63046-5_9","volume-title":"Automated Deduction \u2013 CADE 26","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 130\u2013147. Springer, Cham (2017)"},{"key":"34_CR9","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. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/11814948_8","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2006","author":"T Jussila","year":"2006","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 54\u201360. Springer, Heidelberg (2006)"},{"issue":"C","key":"34_CR12","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.artint.2015.03.004","volume":"224","author":"B Konev","year":"2015","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u0151s discrepancy properties. Artif. Intell. 224(C), 103\u2013118 (2015)","journal-title":"Artif. Intell."},{"key":"34_CR13","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. Discret. Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discret. Appl. Math."},{"key":"34_CR14","unstructured":"Lee, C.T.: A completeness theorem and a computer program for finding theorems derivable from given axioms. Ph.D. thesis (1967)"},{"key":"34_CR15","doi-asserted-by":"crossref","unstructured":"Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing. In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21). EPiC Series in Computing, vol. 46, pp. 65\u201384. EasyChair (2017)","DOI":"10.29007\/7jgq"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/11753728_60","volume-title":"Computer Science \u2013 Theory and Applications","author":"C Sinz","year":"2006","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds.) CSR 2006. LNCS, vol. 3967, pp. 600\u2013611. Springer, Heidelberg (2006)"},{"key":"34_CR17","first-page":"115","volume":"2","author":"GS Tseitin","year":"1968","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. Stud. Math. Math. Log. 2, 115\u2013125 (1968)","journal-title":"Stud. Math. Math. Log."},{"issue":"4","key":"34_CR18","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2178\/bsl\/1203350879","volume":"1","author":"A Urquhart","year":"1995","unstructured":"Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1(4), 425\u2013467 (1995)","journal-title":"Bull. Symb. Log."},{"key":"34_CR19","unstructured":"Van Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: Proceedings of the 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM 2008) (2008)"},{"issue":"4","key":"34_CR20","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Gelder Van","year":"2012","unstructured":"Van Gelder, A.: Producing and verifying extremely large propositional refutations. Ann. Math. Artif. Intell. 65(4), 329\u2013372 (2012)","journal-title":"Ann. Math. Artif. Intell."},{"key":"34_CR21","first-page":"422","volume-title":"Lecture Notes in Computer Science","author":"Nathan Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94205-6_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T12:52:28Z","timestamp":1751719948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94205-6_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319942049","9783319942056"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94205-6_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}