Truly Supercritical Trade-Offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler–Leman
We exhibit supercritical trade-off for monotone circuits, showing that there are functions computable by small circuits for which any small circuit must have depth superlinear 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 an
