Torán, Jacobo ;
Wörz, Florian
Number of Variables for Graph Differentiation and the Resolution of GI Formulas
Abstract
We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by firstorder 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^(k1) and k for the treelike 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 SRC1, 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:136:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772181},
ISSN = {18688969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/15756},
URN = {urn:nbn:de:0030drops157564},
doi = {10.4230/LIPIcs.CSL.2022.36},
annote = {Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, kvariable fragment firstorder logic 𝔏\underlinek, Immerman’s Pebble Game, Symmetry Rule, SRC1}
}
27.01.2022
Keywords: 

Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, kvariable fragment firstorder logic 𝔏_k, Immerman’s Pebble Game, Symmetry Rule, SRC1 
Seminar: 

30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Issue date: 

2022 
Date of publication: 

27.01.2022 