We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Tor\'an and W\"orz (TOCL 2023) showed that there is a resolution refutation of narrow width $k$ for two graphs if and only if they can be distinguished in ($k+1$)-variable first-order logic (FO$^{k+1}$) and hence by a count-free variant of the $k$-dimensional Weisfeiler-Leman algorithm. While DAG-like narrow width $k$ resolution refutations have size at most $n^k$, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width $k$ but only in tree-like size $2^{\Omega(n^{k/2})}$. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical width versus tree-like size trade-off by Razborov (JACM 2016). To prove our result, we develop a new variant of the $k$-pebble EF-game for FO$^k$ to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on a modified variant of the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer (FOCS 2023). Using a recent improved robust compressed CFI construction of Janett, Nordstr\"om, and Pang (unpublished manuscript), we obtain a similar bound for width $k$ (instead of the stronger but less common narrow width) and make the result more robust.

翻译：我们研究了图同构在树状解析演算中的反驳复杂性。Torán和Wörz（TOCL 2023）证明，当且仅当两个图能在（k+1）变量一阶逻辑（FO^{k+1}）中被区分，从而通过k维Weisfeiler-Leman算法的无计数变体区分时，存在宽度为k的窄宽度解析反驳。虽然DAG状的窄宽度k解析反驳的尺寸至多为n^k，但树状反驳的尺寸可能大得多。我们证明存在阶数为n的图，其同构性可在窄宽度k下被反驳，但仅能以树状尺寸2^{Ω(n^{k/2})}实现。这是一种超临界权衡，即限制一个参数（窄宽度）会导致另一个参数（尺寸）增长超过其最坏情况。该尺寸下界相对于公式尺寸是超指数级的，并改进了Razborov（JACM 2016）提出的相关超临界宽度与树状尺寸权衡。为证明我们的结果，我们为FO^k开发了一种新的k-卵石EF博弈变体，以类似于证明复杂性中Prover-Delayer博弈的方式推理树状反驳尺寸。我们在Grohe、Lichter、Neuen和Schweitzer（FOCS 2023）引入的压缩CFI图的修改变体上分析了该博弈。利用Janett、Nordström和Pang（未发表手稿）最近改进的鲁棒压缩CFI构造，我们得到了宽度k（而非更强但不常见的窄宽度）的类似界限，并使结果更具鲁棒性。