An Ultimate Trade-Off in Propositional Proof Complexity

We exhibit an unusually strong trade-off between resolution proof width and tree-like proof size. Namely, we show that for any param-eter k = k(n) there are unsatisfiable k-CNFs that possess refutations of width O(k), but such that any tree-like refutation of width n1−/k must necessarily have double exponential size exp(nΩ(k)). Concep-tually, this means that there exist contradictions that allow narrow refutations, but so that in order to keep the size of a narrow refu-tation even within a single exponent, it must necessarily use a high degree of parallelism. Viewed differently, every tree-like narrow refuta-tion 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 re-sults in a hardness compression approach that strives to preserve hard-ness of a contradiction while significantly decreasing the number of its variables