Under the auspices of the Computational Complexity Foundation (CCF)

REPORTS > KEYWORD > HARDNESS COMPRESSION:
Reports tagged with Hardness compression:
TR15-033 | 6th March 2015
Alexander Razborov

#### An Ultimate Trade-Off in Propositional Proof Complexity

Revisions: 1

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 >>>

ISSN 1433-8092 | Imprint