Alexander Razborov: An ultimate trade-off in propositional proof complexity

Practicalities

Lunch is served at 12:00 noon (register at this doodle at the latest on Saturday March 21). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

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 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 hardness compression approach that strives to preserve hardness of a contradiction while significantly decreasing the number of its variables.