期刊名称：Electronic Colloquium on Computational Complexity
印刷版ISSN：1433-8092
出版年度：2021
卷号：21
语种：English
出版社：Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
摘要：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 minimum number of variables needed to distinguish two graphs with n vertices each, then there is an nO(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2k−1 and k for the tree-like resolution size and resolution clause space for this formula. We also show a resolution size lower bound of exp(k2n) for the case of colored graphs with constant color class size. 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.
关键词：Graph Isomorphism;Immerman's Pebble Game;k-variable fragment first-order logic L_k;Proof Complexity;Resolution
