Document Open Access Logo

Cutting Planes Width and the Complexity of Graph Isomorphism Refutations

Authors Jacobo Torán , Florian Wörz

PDF
Thumbnail PDF

File

LIPIcs.SAT.2023.26.pdf
  • Filesize: 0.86 MB
  • 20 pages

Document Identifiers

Author Details

Jacobo Torán
  • Institut für Theoretische Informatik, Universität Ulm, Germany
Florian Wörz
  • Institut für Theoretische Informatik, Universität Ulm, Germany

Funding

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

Cite AsGet BibTex

Jacobo Torán and Florian Wörz. Cutting Planes Width and the Complexity of Graph Isomorphism Refutations. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.SAT.2023.26

Abstract

The width complexity measure plays a central role in Resolution and other propositional proof systems like Polynomial Calculus (under the name of degree). The study of width lower bounds is the most extended method for proving size lower bounds, and it is known that for these systems, proofs with small width also imply the existence of proofs with small size. Not much has been studied, however, about the width parameter in the Cutting Planes (CP) proof system, a measure that was introduced by Dantchev and Martin in 2011 under the name of CP cutwidth. In this paper, we study the width complexity of CP refutations of graph isomorphism formulas. For a pair of non-isomorphic graphs G and H, we show a direct connection between the Weisfeiler-Leman differentiation number WL(G, H) of the graphs and the width of a CP refutation for the corresponding isomorphism formula Iso(G, H). In particular, we show that if WL(G, H) ≤ k, then there is a CP refutation of Iso(G, H) with width k, and if WL(G, H) > k, then there are no CP refutations of Iso(G, H) with width k-2. Similar results are known for other proof systems, like Resolution, Sherali-Adams, or Polynomial Calculus. We also obtain polynomial-size CP refutations from our width bound for isomorphism formulas for graphs with constant WL-dimension.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
  • Mathematics of computing → Graph theory
Keywords
  • Cutting Planes
  • Proof Complexity
  • Linear Programming
  • Combinatorial Optimization
  • Weisfeiler-Leman Algorithm
  • Graph Isomorphism

Metrics

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

Related Versions

References

  1. 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.
  2. Albert Atserias and Joanna Ochremiak. Definable ellipsoid method, sums-of-squares proofs, and the isomorphism problem. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 18), pages 66-75, 2018. URL: https://doi.org/10.1145/3209108.3209186.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. Christoph Berkholz and Jakob Nordström. Near-optimal lower bounds on quantifier depth and Weisfeiler-Leman refinement steps. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16), pages 267-276, 2016. URL: https://doi.org/10.1145/2933575.2934560.
  8. Béla Bollobás. Distinguishing vertices of random graphs. In North-Holland Mathematics Studies, volume 62, pages 33-49. Elsevier, 1982. URL: https://doi.org/10.1016/S0304-0208(08)73545-X.
  9. Maria L. Bonet, Juan L. Esteban, Nicola Galesi, and Jan Johannsen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM Jornal on Computing, 30(5):1462-1484, 2000. URL: https://doi.org/10.1137/S0097539799352474.
  10. Joshua Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, and Toniann Pitassi. Rank bounds and integrality gaps for cutting planes procedures. Theory Comput., 2(4):65-90, 2006. URL: https://doi.org/10.4086/toc.2006.v002a004.
  11. 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.
  12. Vasek Chvátal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics, 4(4):305-337, 1973. URL: https://doi.org/10.1016/0012-365X(73)90167-2.
  13. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC '96), pages 174-183, May 1996. URL: https://doi.org/10.1145/237814.237860.
  14. Paolo Codenotti, Grant Schoenebeck, and Aaron Snook. Graph isomorphism and the Lasserre hierarchy, 2014. URL: https://arxiv.org/abs/1401.0758.
  15. 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.
  16. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  17. Daniel Dadush and Samarth Tiwari. On the complexity of branching proofs. In Proceedings of the 35th Computational Complexity Conference (CCC '20), volume 169 of LIPIcs, pages 34:1-34:35, 2020. URL: https://doi.org/10.4230/LIPIcs.CCC.2020.34.
  18. Stefan S. Dantchev and Barnaby Martin. Cutting planes and the parameter cutwidth. Theory of Computing Systems, 51(1):50-64, 2012. URL: https://doi.org/10.1007/s00224-011-9373-0.
  19. 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.
  20. Roland Fraïssé. Sur une nouvelle classification des systèmes de relations. Comptes Rendus, 230:1022-1024, 1950. Google Scholar
  21. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. Theory of Computing, 16:1-30, 2020. Earlier conference version in STOC '18. URL: https://doi.org/10.4086/toc.2020.v016a013.
  22. Ralph E. Gomory. An algorithm for integer solutions of linear programs. In R. L. Graves and P. Wolfe, editors, Recent Advances in Mathematical Programming, pages 269-302. McGraw-Hill, New York, 1963. Google Scholar
  23. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. SIAM Journal on Computing, 47(5):1778-1806, 2018. URL: https://doi.org/10.1137/16M1082007.
  24. Martin Grohe. Descriptive Complexity, Canonisation, and Definable Graph Structure Theory, volume 47 of Lecture Notes in Logic. Cambridge University Press, 2017. URL: https://doi.org/10.1017/9781139028868.
  25. Martin Grohe, Moritz Lichter, and Daniel Neuen. The iteration number of the Weisfeiler-Leman algorithm, 2023. URL: https://arxiv.org/abs/2301.13317.
  26. 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.
  27. Armin Haken and Stephen A. Cook. An exponential lower bound for the size of monotone real circuits. Journal of Computer and System Sciences, 58(2):326-335, 1999. URL: https://doi.org/10.1006/jcss.1998.1617.
  28. Philip Hall. On representatives of subsets. Journal of the London Mathematical Society, 10(1):26-30, 1935. URL: https://doi.org/10.1112/jlms/s1-10.37.26.
  29. Lauri Hella. Logical hierarchies in PTIME. Information and Computation, 129(1):1-19, 1996. URL: https://doi.org/10.1006/inco.1996.0070.
  30. Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In Proceedings of the 58th Annual IEEE Symposium on Foundations of Computer Science (FOCS '17), pages 121-131, 2017. URL: https://doi.org/10.1109/FOCS.2017.20.
  31. Trinh Huynh and Jakob Nordström. On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity. In Proceedings of the 44th Symposium on Theory of Computing Conference (STOC '12), pages 233-248, 2012. URL: https://doi.org/10.1145/2213977.2214000.
  32. 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.
  33. Neil Immerman. Descriptive Complexity. Graduate texts in computer science. Springer, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5.
  34. Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS '94), pages 220-228, July 1994. URL: https://doi.org/10.1109/LICS.1994.316069.
  35. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  36. Stasys Jukna. Boolean Function Complexity - Advances and Frontiers, volume 27 of Algorithms and Combinatorics. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24508-4.
  37. Sandra Kiefer. Power and limits of the Weisfeiler-Leman algorithm. Dissertation, RWTH Aachen University, 2020. URL: https://doi.org/10.18154/RWTH-2020-03508.
  38. Sandra Kiefer, Ilia Ponomarenko, and Pascal Schweitzer. The Weisfeiler-Leman dimension of planar graphs is at most 3. Journal of the ACM, 66(6):44:1-44:31, 2019. URL: https://doi.org/10.1145/3333003.
  39. Ludek Kucera. Canonical labeling of regular graphs in linear average time. In Proceedings of the 28th Annual IEEE Symposium on Foundations of Computer Science (FOCS '87), pages 271-279, 1987. URL: https://doi.org/10.1109/SFCS.1987.11.
  40. Massimo Lauria. A rank lower bound for cutting planes proofs of Ramsey’s theorem. ACM Transactions on Computation Theory, 8(4):17:1-17:13, 2016. URL: https://doi.org/10.1145/2903266.
  41. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science: An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07003-1.
  42. 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.
  43. Noam Nisan. CREW PRAMs and decision trees. SIAM Journal on Computing, 20(6):999-1007, 1991. URL: https://doi.org/10.1137/0220062.
  44. 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.
  45. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  46. Alexander A. Razborov. On the width of semialgebraic proofs and algorithms. Math. Oper. Res., 42(4):1106-1134, 2017. URL: https://doi.org/10.1287/moor.2016.0840.
  47. Alexander Schrijver. On cutting planes. Annals of Discrete Mathematics, 9:291-296, 1980. URL: https://doi.org/10.1016/S0167-5060(08)70085-2.
  48. 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), volume 187 of LIPIcs, pages 58:1-58:16, 2021. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.58.
  49. Hanif D. Sherali and Warren P. Adams. A hierarchy of relaxations between the continuous and convex hull representations for zero-one programming problems. SIAM Journal on Discrete Mathematics, 3(3):411-430, 1990. URL: https://doi.org/10.1137/0403036.
  50. Jacobo Torán. On the hardness of graph isomorphism. SIAM Journal on Computing, 33(5):1093-1108, 2004. URL: https://doi.org/10.1137/S009753970241096X.
  51. 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.
  52. Jacobo Torán and Florian Wörz. Number of variables for graph differentiation and the resolution of graph isomorphism formulas. ACM Transactions on Computational Logic, 24(3):23:1-23:25, April 2023. Earlier conference version in CSL '22. URL: https://doi.org/10.1145/3580478.
  53. Alasdair Urquhart. The symmetry rule in propositional logic. Discrete Applied Mathematics, 96-97:177-193, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00039-6.
  54. Alasdair Urquhart. The depth of resolution proofs. Studia Logica, 99(1-3):349-364, 2011. URL: https://doi.org/10.1007/s11225-011-9356-9.
  55. Boris Weisfeiler. On Construction and Identification of Graphs, volume 558 of Lecture Notes in Mathematics. Springer, 1976. URL: https://doi.org/10.1007/BFb0089374.
  56. 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