Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR15-033 | 13th November 2015 18:10

An Ultimate Trade-Off in Propositional Proof Complexity

RSS-Feed




Revision #1
Authors: Alexander Razborov
Accepted on: 13th November 2015 18:10
Downloads: 299
Keywords: 


Abstract:

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, this means that there exist contradictions that allow narrow refutations, but in order to keep the size of such a refutation even within a single exponent, it must necessarily use a high degree of parallelism. Viewed differently, every tree-like narrow refutation is exponentially worse not only than wide refutations of the same contradiction, but of any other contradiction with the same number of variables. This seems to significantly deviate from the established pattern of most, if not all, trade-off results in complexity theory.

Our construction and proof methods combine, in a non-trivial way, two previously known techniques: the hardness escalation method based on substitution formulas and expansion. This combination results in a {\em hardness compression} approach that strives to preserve hardness of a contradiction while significantly decreasing the number of its variables.



Changes to previous version:

Introduction has been significantly
expanded. A few typos fixed.


Paper:

TR15-033 | 6th March 2015 16:31

An Ultimate Trade-Off in Propositional Proof Complexity





TR15-033
Authors: Alexander Razborov
Publication: 6th March 2015 16:32
Downloads: 711
Keywords: 


Abstract:

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, this means that there exist contradictions that allow narrow refutations, but in order to keep the size of such a refutation even within a single exponent, it must necessarily use a high degree of parallelism. Viewed differently, every tree-like narrow refutation is exponentially worse not only than wide refutations of the same contradiction, but of any other contradiction with the same number of variables. This seems to significantly deviate from the established pattern of most, if not all, trade-off results in complexity theory.

Our construction and proof methods combine, in a non-trivial way, two previously known techniques: the hardness escalation method based on substitution formulas and expansion. This combination results in a {\em hardness compression} approach that strives to preserve hardness of a contradiction while significantly decreasing the number of its variables.



ISSN 1433-8092 | Imprint