Supercritical and Robust Trade-offs for Resolution Depth Versus Width and Weisfeiler–Leman

We give the first robust resolution trade-offs for which low width implies depth superlinear in the formula size. We show analogous results for the Weisfeiler–Leman algorithm, which also translate into trade-offs between number of variables and quantifier depth in first-order logic. Our main technical contribution is a new compression scheme and analysis of the so-called compressed Cop-Robber game introduced by [Grohe et al., FOCS 2023].