eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
36:1
36:18
10.4230/LIPIcs.CSL.2022.36
article
Number of Variables for Graph Differentiation and the Resolution of GI Formulas
Torán, Jacobo
1
https://orcid.org/0000-0003-2168-4969
Wörz, Florian
1
https://orcid.org/0000-0003-2463-8167
Universität Ulm, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.36/LIPIcs.CSL.2022.36.pdf
Proof Complexity
Resolution
Narrow Width
Graph Isomorphism
k-variable fragment first-order logic 𝔏_k
Immerman’s Pebble Game
Symmetry Rule
SRC-1