Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and Weisfeiler–Leman

Susanna de Rezende ( Lund University )

We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any circuit must have depth super-linear or even super-polynomial in the number of variables, far exceeding the linear worst-case upper bound. We obtain similar trade-offs in proof complexity, where we establish the first size-depth trade-offs for cutting planes and resolution that are truly supercritical, i.e., in terms of formula size rather than number of variables, and we also show supercritical trade-offs between width and size for treelike resolution.

Our results build on a new supercritical depth-width trade-off for resolution, obtained by refining and strengthening the compression scheme for the cop-robber game in [Grohe, Lichter, Neuen & Schweitzer 2023]. This yields robust supercritical trade-offs for dimension versus iteration number in the Weisfeiler–Leman algorithm. Our other results follow from improved lifting theorems that might be of independent interest.

This is joint work with Noah Fleming, Duri Andrea Janett, Jakob Nordström, and Shuo Pang.