2026-07-26T12:38:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24125 2025-11-12T13:33:21Z ddc:004 open_access

Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism Berkholz, Christoph Lichter, Moritz Vinall-Smeeth, Harry Proof complexity Resolution Width Tree-like size Supercritical trade-off Lower bound Finite model theory CFI graphs We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz [Jacobo Torán and Florian Wörz, 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}). 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^{Ω(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 trade-off by Razborov [Alexander A. Razborov, 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 the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer [Martin Grohe et al., 2023]. Using a recent improved robust compressed CFI construction of de Rezende, Fleming, Janett, Nordström, and Pang [Susanna F. de Rezende et al., 2024], we obtain a similar bound for width k (instead of the stronger but less common narrow width) and make the result more robust. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Christoph Berkholz and Moritz Lichter and Harry Vinall-Smeeth 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.18 urn:nbn:de:0030-drops-241253 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.18 eng https://creativecommons.org/licenses/by/4.0/legalcode