### A New Kind of Tradeoffs in Propositional Proof ComplexityA New Kind of Tradeoffs in Propositional Proof Complexity

Access Restriction
Subscribed

 Author Razborov, Alexander Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2016 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword Hardness compression ♦ Resolution ♦ Tradeoff Abstract We exhibit an unusually strong tradeoff in propositional proof complexity that significantly deviates from the established pattern of almost all results of this kind. Namely, restrictions on one resource (width, in our case) imply an increase in another resource (tree-like size) that is exponential not only with respect to the complexity of the original problem, but also to the whole class of $\textit{all}$ problems of the same bit size. More specifically, we show that for any parameter $\textit{k}$ = $\textit{k}(\textit{n}),$ there are unsatisfiable $\textit{k}-CNFs$ that possess refutations of width $\textit{O}(\textit{k}),$ but such that any tree-like refutation of width $\textit{n}1$ ™ $ε/\textit{k}$ must necessarily have $\textit{doubly}$ exponential size $exp (n^{Ω(k)}).$ 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. 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 hardness compression approach that strives to preserve hardness of a contradiction while significantly decreasing the number of its variables. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2016-04-07 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 63 Issue Number 2 Page Count 14 Starting Page 1 Ending Page 14

#### Open content in new tab

Source: ACM Digital Library