{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T19:06:14Z","timestamp":1784574374890,"version":"3.55.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T00:00:00Z","timestamp":1596153600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T00:00:00Z","timestamp":1596153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF- 1910438"],"award-info":[{"award-number":["CCF- 1910438"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["W1255-N23"],"award-info":[{"award-number":["W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["VRG11-005"],"award-info":[{"award-number":["VRG11-005"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-103"],"award-info":[{"award-number":["ICT15-103"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006112","name":"Microsoft Research","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006112","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution\u2014introduced by Tseitin in the sixties\u2014allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that\u2014from the viewpoint of proof complexity\u2014these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann\u2019s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems.<\/jats:p>","DOI":"10.1007\/s10817-020-09554-z","type":"journal-article","created":{"date-parts":[[2020,7,31]],"date-time":"2020-07-31T01:02:53Z","timestamp":1596157373000},"page":"1247-1267","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Simulating Strong Practical Proof Systems with Extended Resolution"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3522-3653","authenticated-orcid":false,"given":"Benjamin","family":"Kiesl","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adri\u00e1n","family":"Rebola-Pardo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,7,31]]},"reference":[{"issue":"1\u20133","key":"9554_CR1","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1016\/S0304-3975(03)00395-5","volume":"310","author":"M Alekhnovich","year":"2004","unstructured":"Alekhnovich, M.: Mutilated chessboard problem is exponentially hard for resolution. Theoret. Comput. Sci. 310(1\u20133), 513\u2013525 (2004)","journal-title":"Theoret. Comput. Sci."},{"key":"9554_CR2","volume-title":"Methods of Cut-Elimination. No.\u00a03 in Trends in Logic","author":"M Baaz","year":"2011","unstructured":"Baaz, M., Leitsch, A.: Methods of Cut-Elimination. No.\u00a03 in Trends in Logic. Springer, Berlin (2011)"},{"key":"9554_CR3","unstructured":"Biere, A.: Two pigeons per hole problem. In: Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions, p. 103 (2013)"},{"key":"9554_CR4","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)"},{"issue":"4","key":"9554_CR5","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":"9554_CR6","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":"9554_CR7","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Hunt, W. A. Jr.., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26). LNCS, vol. 10395, pp. 220\u2013236. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"9554_CR8","doi-asserted-by":"crossref","unstructured":"Dantchev, S.S,. Riis, S.: \u201cPlanar\u201d tautologies hard for resolution. In: Proceedings of the 42nd Annual Symposium on Foundations of Computer Science (FOCS 2001), pp. 220\u2013229. IEEE Computer Society, New York (2001)","DOI":"10.1109\/SFCS.2001.959896"},{"key":"9554_CR9","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. Theoret. Comput. Sci. 39, 297\u2013308 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"9554_CR10","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Biere, A.: What a difference a variable makes. In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u00a02018), LNCS, vol. 10806, pp. 75\u201392. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-89963-3_5"},{"key":"9554_CR11","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02016). LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-40970-2_15"},{"key":"9554_CR12","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Hunt, W.A. Jr., Kaufmann, M., Wetzler, N.D.: Efficient, verified checking of propositional proofs. In: Proceedings of the 8th International Conference on Interactive Theorem Proving (ITP 2017). LNCS, vol. 10499, pp. 269\u2013284. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-66107-0_18"},{"key":"9554_CR13","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: Proceedings of the 26th International Conference on Automated Deduction (CADE-26), LNCS, vol. 10395, pp. 130\u2013147. Springer, Cham (2017)","DOI":"10.1007\/978-3-319-63046-5_9"},{"key":"9554_CR14","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Seidl, M., Biere, A.: PRuning through satisfaction. In: Proceedings of the 13th Haifa Verification Conference (HVC 2017). LNCS, vol. 10629, pp. 179\u2013194. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-70389-3_12"},{"key":"9554_CR15","doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Encoding redundancy for satisfaction-driven clause learning. In: Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). LNCS, vol. 11427, pp. 41\u201358. Springer, Berlin (2019)","DOI":"10.1007\/978-3-030-17462-0_3"},{"key":"9554_CR16","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/s10817-019-09516-0","volume":"64","author":"MJH Heule","year":"2019","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Strong extension-free proof systems. J. Autom. Reason. 64, 533\u2013554 (2019b)","journal-title":"J. Autom. Reason."},{"key":"9554_CR17","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.J.H.: Blocked clause elimination. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010). LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-12002-2_10"},{"key":"9554_CR18","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR\u00a02012). LNCS, vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31365-3_28"},{"key":"9554_CR19","doi-asserted-by":"crossref","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006). LNCS, vol. 4121, pp. 54\u201360. Springer, Berlin (2006)","DOI":"10.1007\/11814948_8"},{"key":"9554_CR20","doi-asserted-by":"crossref","unstructured":"Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR 2018). LNCS, vol. 10900, pp. 516\u2013531. Springer, Berlin (2018)","DOI":"10.1007\/978-3-319-94205-6_34"},{"issue":"C","key":"9554_CR21","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":"9554_CR22","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 Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"9554_CR23","unstructured":"Lee, C.T.: A completeness theorem and a computer program for finding theorems derivable from given axioms. Ph.D. Thesis, University of California, Berkeley (1967)"},{"issue":"5","key":"9554_CR24","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"JP Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"9554_CR25","unstructured":"McCarthy, J.: A tough nut for proof procedures. Memo 16, Stanford Artificial Intelligence Project (1964)"},{"key":"9554_CR26","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535. ACM, New York (2001)","DOI":"10.1145\/378239.379017"},{"key":"9554_CR27","unstructured":"Philipp, T., Rebola-Pardo, A.: Towards a semantics of unsatisfiability proofs with inprocessing. In: Procedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21), EasyChair, EPiC Series in Computing, vol. 46, pp. 65\u201384 (2017)"},{"key":"9554_CR28","unstructured":"Rebola-Pardo, A., Suda, M.: A theory of satisfiability-preserving proofs in SAT solving. In: Proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-22), EasyChair, EPiC Series in Computing, vol. 57, pp. 583\u2013603 (2018)"},{"key":"9554_CR29","doi-asserted-by":"crossref","unstructured":"Sinz, C., Biere, A.: Extended resolution proofs for conjoining BDDs. In: Proceedings of the 1st International Computer Science Symposium in Russia (CSR 2006). LNCS, vol. 3967, pp. 600\u2013611. Springer, Heidelberg (2006)","DOI":"10.1007\/11753728_60"},{"key":"9554_CR30","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":"1","key":"9554_CR31","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (1987)","journal-title":"J. ACM"},{"issue":"4","key":"9554_CR32","doi-asserted-by":"publisher","first-page":"425","DOI":"10.2307\/421131","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":"9554_CR33","unstructured":"Van\u00a0Gelder, A.: Verifying RUP proofs of propositional unsatisfiability. In: Proceedings of the 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM\u00a02008) (2008)"},{"issue":"4","key":"9554_CR34","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Van Gelder","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":"9554_CR35","doi-asserted-by":"crossref","unstructured":"Wetzler, N.D., Heule, M.J.H., Hunt, W.A. Jr: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT\u00a02014). LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014)","DOI":"10.1007\/978-3-319-09284-3_31"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09554-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09554-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09554-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,31]],"date-time":"2021-07-31T00:00:09Z","timestamp":1627689609000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09554-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,31]]},"references-count":35,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2020,10]]}},"alternative-id":["9554"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09554-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,7,31]]},"assertion":[{"value":"17 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 April 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}