Document Open Access Logo

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

Authors Jacobo Torán , Florian Wörz

PDF
Thumbnail PDF

File

LIPIcs.CSL.2022.36.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Jacobo Torán
  • Universität Ulm, Germany
Florian Wörz
  • Universität Ulm, Germany

Funding

This research was supported by the Deutsche Forschungsgemeinschaft (DFG) under project number 430150230, "Complexity measures for solving propositional formulas".

Acknowledgements

We thank Pascal Schweitzer for helpful discussions. We would also like to thank the anonymous reviewers for many insightful comments and suggestions.

Cite AsGet BibTex

Jacobo Torán and Florian Wörz. Number of Variables for Graph Differentiation and the Resolution of GI Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CSL.2022.36

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
  • Mathematics of computing → Graph theory
Keywords
  • Proof Complexity
  • Resolution
  • Narrow Width
  • Graph Isomorphism
  • k-variable fragment first-order logic 𝔏_k
  • Immerman’s Pebble Game
  • Symmetry Rule
  • SRC-1

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Noriko H. Arai and Alasdair Urquhart. Local symmetries in propositional logic. In Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2000, St Andrews, Scotland, UK, July 3-7, 2000, Proceedings, pages 40-51, 2000. URL: https://doi.org/10.1007/10722086_3.
  2. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, 2008. Earlier conference version in CCC '03. URL: https://doi.org/10.1016/j.jcss.2007.06.025.
  3. Albert Atserias and Elitza N. Maneva. Sherali-Adams relaxations and indistinguishability in counting logics. SIAM Journal on Computing, 42(1):112-137, 2013. Earlier conference version in ITCS '12. URL: https://doi.org/10.1137/120867834.
  4. László Babai. Graph isomorphism in quasipolynomial time [extended abstract]. In Proceedings of the 48th Annual ACM SIGACT Symposium on Theory of Computing (STOC '16), pages 684-697, 2016. Full-length version in arXiv:1512.03547. URL: https://doi.org/10.1145/2897518.2897542.
  5. László Babai and Shlomo Moran. Arthur-Merlin games: A randomized proof system, and a hierarchy of complexity classes. Journal of Computer and System Sciences, 36(2):254-276, 1988. URL: https://doi.org/10.1016/0022-0000(88)90028-1.
  6. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. Earlier conference versions in STOC '99 and CCC '99. URL: https://doi.org/10.1145/375827.375835.
  7. Christoph Berkholz and Martin Grohe. Limitations of algebraic approaches to graph isomorphism testing. In Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP '15), pages 155-166, 2015. URL: https://doi.org/10.1007/978-3-662-47672-7_13.
  8. Jin-yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identifications. Combinatorica, 12(4):389-410, 1992. Earlier conference version in FOCS '89. URL: https://doi.org/10.1007/BF01305232.
  9. Paolo Codenotti, Grant Schoenebeck, and Aaron Snook. Graph isomorphism and the Lasserre hierarchy. arXiv, 1401.0758, 2014. URL: http://arxiv.org/abs/1401.0758.
  10. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  11. Anuj Dawar and Kashif Khan. Constructing hard examples for graph isomorphism. Journal of Graph Algorithms and Applications, 23(2):293-316, 2019. URL: https://doi.org/10.7155/jgaa.00492.
  12. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141, 1961. URL: https://doi.org/10.4064/fm-49-2-129-141.
  13. Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theoretical Computer Science, 321(2-3):347-370, 2004. Earlier conference version in ICALP '02. URL: https://doi.org/10.1016/j.tcs.2004.04.004.
  14. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171(1):84-97, 2001. Preliminary versions in STACS '99 and CSL '99. URL: https://doi.org/10.1006/inco.2001.2921.
  15. Roland Fraïssé. Sur une nouvelle classification des systèmes de relations. Comptes Rendus, 230:1022-1024, 1950. Google Scholar
  16. Merrick L. Furst, John E. Hopcroft, and Eugene M. Luks. Polynomial-time algorithms for permutation groups. In Proceedings of the 21st Annual Symposium on Foundations of Computer Science (FOCS), pages 36-41, 1980. URL: https://doi.org/10.1109/SFCS.1980.34.
  17. Nicola Galesi and Neil Thapen. Resolution and pebbling games. In Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing (SAT '05), pages 76-90, 2005. URL: https://doi.org/10.1007/11499107_6.
  18. Martin Grohe and Martin Otto. Pebble games and linear equations. The Journal of Symbolic Logic, 80(3):797-844, 2015. Earlier conference version in CSL '12. URL: https://doi.org/10.1017/jsl.2015.28.
  19. Yuri Gurevich and Saharon Shelah. On finite rigid structures. The Journal of Symbolic Logic, 61(2):549-562, 1996. URL: https://doi.org/10.2307/2275675.
  20. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. URL: https://doi.org/10.1016/0304-3975(85)90144-6.
  21. Neil Immerman. Upper and lower bounds for first order expressibility. Journal of Computer and System Sciences, 25(1):76-98, 1982. Earlier conference version in FOCS '80. URL: https://doi.org/10.1016/0022-0000(82)90011-3.
  22. Neil Immerman. Descriptive Complexity. Graduate texts in computer science. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5.
  23. Sandra Kiefer. Power and limits of the Weisfeiler-Leman algorithm. Dissertation, RWTH Aachen University, 2020. URL: https://doi.org/10.18154/RWTH-2020-03508.
  24. Sandra Kiefer. The Weisfeiler-Leman algorithm: an exploration of its power. ACM SIGLOG News, 7(3):5-27, 2020. URL: https://doi.org/10.1145/3436980.3436982.
  25. Pavel Klavík, Dusan Knop, and Peter Zeman. Graph isomorphism restricted by lists. Theoretical Computer Science, 860:51-71, 2021. Earlier conference version in WG '20. URL: https://doi.org/10.1016/j.tcs.2021.01.027.
  26. Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta Informatica, 22(3):253-275, 1985. URL: https://doi.org/10.1007/BF00265682.
  27. Anna Lubiw. Some NP-complete problems similar to graph isomorphism. SIAM Journal on Computing, 10(1):11-21, 1981. URL: https://doi.org/10.1137/0210002.
  28. Peter N. Malkin. Sherali-Adams relaxations of graph isomorphism polytopes. Discrete Optimization, 12:73-97, 2014. URL: https://doi.org/10.1016/j.disopt.2014.01.004.
  29. Daniel Neuen and Pascal Schweitzer. An exponential lower bound for individualization-refinement algorithms for graph isomorphism. In Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing (STOC '18), pages 138-150. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188900.
  30. Ryan O'Donnell, John Wright, Chenggang Wu, and Yuan Zhou. Hardness of robust graph isomorphism, lasserre gaps, and asymmetry of random graphs. In Proceedings of the 25th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA '14), pages 1659-1677, 2014. URL: https://doi.org/10.1137/1.9781611973402.120.
  31. Theodoros Papamakarios and Alexander Razborov. Space characterizations of complexity measures and size-space trade-offs in propositional proof systems. Technical Report TR21-074, ECCC, 2021. URL: https://eccc.weizmann.ac.il/report/2021/074/.
  32. Alexander A. Razborov. Proof complexity of pigeonhole principles. In Proceedings of the 5th International Conference on Developments in Language Theory (DLT '01), Revised Papers, pages 100-116, 2001. URL: https://doi.org/10.1007/3-540-46011-X_8.
  33. Pascal Schweitzer and Constantin Seebach. Resolution with symmetry rule applied to linear equations. In Proceedings of the 38th International Symposium on Theoretical Aspects of Computer Science (STACS '21), pages 58:1-58:16, 2021. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.58.
  34. Hanif D. Sherali and Warren P. Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM J. Discret. Math., 3(3):411-430, 1990. URL: https://doi.org/10.1137/0403036.
  35. Stefan Szeider. The complexity of resolution with generalized symmetry rules. Theory of Computing Systems, 38(2):171-188, 2005. Earlier conference version in STACS '03. URL: https://doi.org/10.1007/s00224-004-1192-0.
  36. Jacobo Torán. On the resolution complexity of graph non-isomorphism. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT '13), pages 52-66, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_6.
  37. Jacobo Torán and Florian Wörz. Number of variables for graph identification and the resolution of GI formulas. Technical Report TR21-097, ECCC, 2021. URL: https://eccc.weizmann.ac.il/report/2021/097.
  38. Grigori S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2, volume 8 of Seminars in Mathematics, pages 115-125. Consultants Bureau, 1968. Google Scholar
  39. Alasdair Urquhart. The symmetry rule in propositional logic. Discret. Appl. Math., 96-97:177-193, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00039-6.
  40. Boris Weisfeiler. On Construction and Identification of Graphs, volume 558 of Lecture Notes in Mathematics. Springer, 1976. URL: https://doi.org/10.1007/BFb0089374.
  41. Boris Weisfeiler and Andrei Leman. The reduction of a graph to canonical form and the algebra which appears therein. Nauchno-Technicheskaya Informatsia, Seriya 2, 9, 1968. Translation from Russian into English by Grigory Ryabov available under URL: https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact