Search Results

Documents authored by Vinall-Smeeth, Harry

Document
DOI: 10.4230/LIPIcs.MFCS.2025.18
Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

Authors: Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
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.
Cite as

Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.MFCS.2025.18,
  author =	{Berkholz, Christoph and Lichter, Moritz and Vinall-Smeeth, Harry},
  title =	{{Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{18:1--18:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.18},
  URN =		{urn:nbn:de:0030-drops-241253},
  doi =		{10.4230/LIPIcs.MFCS.2025.18},
  annote =	{Keywords: Proof complexity, Resolution, Width, Tree-like size, Supercritical trade-off, Lower bound, Finite model theory, CFI graphs}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.113
A Dichotomy for Succinct Representations of Homomorphisms

Authors: Christoph Berkholz and Harry Vinall-Smeeth

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
The task of computing homomorphisms between two finite relational structures A and B is a well-studied question with numerous applications. Since the set Hom(A, B) of all homomorphisms may be very large having a method of representing it in a succinct way, especially one which enables us to perform efficient enumeration and counting, could be extremely useful. One simple yet powerful way of doing so is to decompose Hom(A, B) using union and Cartesian product. Such data structures, called d-representations, have been introduced by Olteanu and Závodný [Olteanu and Závodný, 2015] in the context of database theory. Their results also imply that if the treewidth of the left-hand side structure A is bounded, then a d-representation of polynomial size can be found in polynomial time. We show that for structures of bounded arity this is optimal: if the treewidth is unbounded then there are instances where the size of any d-representation is superpolynomial. Along the way we develop tools for proving lower bounds on the size of d-representations, in particular we define a notion of reduction suitable for this context and prove an almost tight lower bound on the size of d-representations of all k-cliques in a graph.
Cite as

Christoph Berkholz and Harry Vinall-Smeeth. A Dichotomy for Succinct Representations of Homomorphisms. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 113:1-113:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.ICALP.2023.113,
  author =	{Berkholz, Christoph and Vinall-Smeeth, Harry},
  title =	{{A Dichotomy for Succinct Representations of Homomorphisms}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{113:1--113:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.113},
  URN =		{urn:nbn:de:0030-drops-181653},
  doi =		{10.4230/LIPIcs.ICALP.2023.113},
  annote =	{Keywords: homomorphism problem, CSP, succinct representations, enumeration, lower bound, treewidth}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact