Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

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ᵏ, 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^ (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ᵏ 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.