We present the best known separation between tree-like and general resolution, improving on the recent exp(n ∈) separation of [2]. This is done by constructing a natural family of contradictions, of size n, that have O(n)-size resolution refutations, but only exp(Ω(n/log n))- size tree-like refutations. This result implies that the most commonly used automated theorem procedures, which produce tree-like resolution refutations, will perform badly on some inputs, while other simple procedures, that produce general resolution refutations, will have polynomial run-time on these very same inputs. We show, furthermore that the gap we present is nearly optimal. Specifically, if S (S T ) is the minimal size of a (tree-like) refutation, we prove that S T = exp(O(S log log S/log S)).
Article PDF
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Corresponding author
Additional information
* This research was supported by Clore Foundation Doctoral Scholarship.
† Research supported by NSF Award CCR-0098197 and USA–Israel BSF Grant 97-00188.
‡ This research was supported by grant number 69/96 of the Israel Science Foundation, founded by the Israel Academy for Sciences and Humanities.
Rights and permissions
About this article
Cite this article
Ben-Sasson*, E., Impagliazzo†, R. & Wigderson‡, A. Near Optimal Separation Of Tree-Like And General Resolution. Combinatorica 24, 585–603 (2004). https://doi.org/10.1007/s00493-004-0036-5
Received:
Issue Date:
DOI: https://doi.org/10.1007/s00493-004-0036-5