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 width-depth 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, which also translate into trade-offs between number of variables and quantifier depth in first-order logic. Our other results follow from improved lifting theorems that might be of independent interest.

翻译：我们展示了单调电路的超临界权衡，证明存在可由小型电路计算的函数，其任何电路的深度必须远超过变量数量的线性甚至超多项式增长，大幅突破了线性最坏情况上界。在证明复杂性领域，我们获得了类似的权衡结果：首次针对割平面与分辨率建立了真正超临界（即依据公式规模而非变量数量）的规模-深度权衡，并证明了树状分辨率中宽度与规模间的超临界权衡。这些结果基于我们新提出的分辨率超临界宽度-深度权衡，该结论通过精化并强化[Grohe, Lichter, Neuen & Schweitzer 2023]中警察-盗贼博弈的压缩方案而获得。由此产生了Weisfeiler-Leman算法中维度与迭代次数的鲁棒超临界权衡，该结果可转化为一阶逻辑中变量数量与量词深度的权衡关系。其余结论源自可能具有独立价值的改进提升定理。