Truly Supercritical Trade-offs for Resolution, Cutting Planes, Monotone Circuits, and Weisfeiler-Leman

Abstract

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.

Figures (7)

• Figure 1: An illustration of trade-offs. Blue dots represent provable upper bounds on measures $\mu$ and $\nu$. Proofs with measures in the shaded region are ruled out by the trade-off, where $\mu_{\textrm{worst}}$ and $\nu_{\textrm{worst}}$ are the worst-case upper bound on $\mu$ and $\nu$, respectively. \ref{['fig:nonsuper']} illustrates a non-supercritical trade-off and \ref{['fig:super']} illustrates a supercritical one.
• Figure 2: Hardness condensation in \ref{['fig:xor']} substitutes the $x$-variables with an XOR over some $y$-variables, while variable compression in \ref{['fig:ident']} substitutes with $y$-variables directly. Note that $m\ll n$.
• Figure 3: The compression of two rows in the middle part is depicted. The parameters are chosen as $L=P_1 \cdot P_2 \cdot P_3 = 2 \cdot 3 \cdot 5$, $c=1$, $m_1=P_1\cdot P_2 = 6$, and $m_2=P_2\cdot P_3 = 15$. Equivalent vertical edges are drawn in the same color.
• Figure 4: A special move $P$ starting in column $a$ is shown as the segmented path, where $I$ is the underlying row set.
• Figure 5: The green circles are vertices in $W_\equiv$ (i.e., they are in the equivalent classes of the Cops). The red and blue curves illustrate two minimal vertex separators contained in $W_\equiv$. The yellow region represents all virtual cordons associated with $W$.

Theorems & Definitions (83)

• Theorem 0: Monotone circuit trade-offs
• Theorem 0: Cutting planes trade-offs
• theorem 1: Width-size trade-offs
• Theorem 0: Width-depth trade-offs
• Theorem 0: Weisfeiler--Leman trade-offs
• Theorem 0: Cop-Robber
• theorem 2: Weisfeiler--Leman trade-offs, explicit
• theorem 3: Width-depth trade-offs, general
• Theorem 0: Lifting for treelike resolution
• theorem 4: Width-size trade-offs, general