@article{BenSasson-Impagliazzo-Wigderson:Combinatorica:2004,
    Abstract = {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 (ST) is the minimal size of a (tree-like) refutation, we prove that ST= exp(O(S log log S/log S)).},
    Author = {Ben-Sasson, Eli and Impagliazzo, Russell and Wigderson, Avi},
    File = {Near Optimal Separation Of Tree-Like And General Resolution - 10.1007@s00493-004-0036-5.pdf},
    ISBN = {1439-6912},
    Journal = {Combinatorica},
    Number = {4},
    Pages = {585--603},
    Title = {Near Optimal Separation Of Tree-Like And General Resolution},
    URL = {https://doi.org/10.1007/s00493-004-0036-5},
    Volume = {24},
    Year = {2004},
    bdsk-url-1 = {https://doi.org/10.1007/s00493-004-0036-5},
    da = {2004/09/01},
    date-added = {2021-08-04 10:31:25 +0200},
    date-modified = {2021-08-04 10:32:06 +0200},
    id = {Ben-Sasson*2004},
    ty = {JOUR},
    doi = {10.1007/s00493-004-0036-5}
}

@article{BenSasson-Impagliazzo-Wigderson:Combinatorica:2004, Abstract = {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 (ST) is the minimal size of a (tree-like) refutation, we prove that ST= exp(O(S log log S/log S)).}, Author = {Ben-Sasson, Eli and Impagliazzo, Russell and Wigderson, Avi}, File = {Near Optimal Separation Of Tree-Like And General Resolution - 10.1007@s00493-004-0036-5.pdf}, ISBN = {1439-6912}, Journal = {Combinatorica}, Number = {4}, Pages = {585--603}, Title = {Near Optimal Separation Of Tree-Like And General Resolution}, URL = {https://doi.org/10.1007/s00493-004-0036-5}, Volume = {24}, Year = {2004}, bdsk-url-1 = {https://doi.org/10.1007/s00493-004-0036-5}, da = {2004/09/01}, date-added = {2021-08-04 10:31:25 +0200}, date-modified = {2021-08-04 10:32:06 +0200}, id = {Ben-Sasson*2004}, ty = {JOUR}, doi = {10.1007/s00493-004-0036-5} }