ECCC-Report TR00-005https://eccc.weizmann.ac.il/report/2000/005Comments and Revisions published for TR00-005en-usThu, 20 Jan 2000 10:23:12 +0200
Paper TR00-005
| Near-Optimal Separation of Treelike and General Resolution |
Eli Ben-Sasson,
Russell Impagliazzo,
Avi Wigderson
https://eccc.weizmann.ac.il/report/2000/005We present the best known separation
between tree-like and general resolution, improving
on the recent $\exp(n^\epsilon)$ separation of \cite{BEGJ98}.
This is done by constructing a natural family of contradictions, of
size $n$, that have $O(n)$-size resolution
refutations, but only $\exp (\Omega(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 of some inputs, while other simple procedures,
that produce general resolution refutations,
will have polynomial runtime 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))$.
Thu, 20 Jan 2000 10:23:12 +0200https://eccc.weizmann.ac.il/report/2000/005