TR00-005 Authors: Eli Ben-Sasson, Russell Impagliazzo, Avi Wigderson

Publication: 20th January 2000 10:23

Downloads: 1948

Keywords:

We 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))$.