Alexander Razborov

We exhibit an unusually strong trade-off between resolution proof width and tree-like proof size. Namely, we show that for any parameter $k=k(n)$ there are unsatisfiable $k$-CNFs that possess refutations of width $O(k)$, but such that any tree-like refutation of width $n^{1-\epsilon}/k$ must necessarily have {\em double} exponential size $\exp(n^{\Omega(k)})$. Conceptually, ... more >>>