License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2022.36
URN: urn:nbn:de:0030-drops-157564
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15756/
Go to the corresponding LIPIcs Volume Portal

Torán, Jacobo ; Wörz, Florian

Number of Variables for Graph Differentiation and the Resolution of GI Formulas

pdf-format:
LIPIcs-CSL-2022-36.pdf (0.8 MB)

Abstract

We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and positive depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution.
Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the number of variables needed to distinguish two graphs with n vertices each, then there is an n^O(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2^(k-1) and k for the tree-like resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp(Ω(k²/n)) for the case of colored graphs with constant color class sizes.
Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach.

BibTeX - Entry

@InProceedings{toran_et_al:LIPIcs.CSL.2022.36,
  author =	{Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
  title =	{{Number of Variables for Graph Differentiation and the Resolution of GI Formulas}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15756},
  URN =		{urn:nbn:de:0030-drops-157564},
  doi =		{10.4230/LIPIcs.CSL.2022.36},
  annote =	{Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, k-variable fragment first-order logic ?\underlinek, Immerman’s Pebble Game, Symmetry Rule, SRC-1}
}

Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, k-variable fragment first-order logic ?_k, Immerman’s Pebble Game, Symmetry Rule, SRC-1
Collection: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
Issue Date: 2022
Date of publication: 27.01.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI