Document Open Access Logo

Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism

Authors Christoph Berkholz , Moritz Lichter , Harry Vinall-Smeeth

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.18.pdf
  • Filesize: 0.85 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • Resolution
  • Width
  • Tree-like size
  • Supercritical trade-off
  • Lower bound
  • Finite model theory
  • CFI graphs

Metrics

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

Abstract

We study the refutation complexity of graph isomorphism in the tree-like resolution calculus. Torán and Wörz [Jacobo Torán and Florian Wörz, 2023] showed that there is a resolution refutation of narrow width k for two graphs if and only if they can be distinguished in (k+1)-variable first-order logic (FO^{k+1}). While DAG-like narrow width k resolution refutations have size at most n^k, tree-like refutations may be much larger. We show that there are graphs of order n, whose isomorphism can be refuted in narrow width k but only in tree-like size 2^{Ω(n^{k/2})}. This is a supercritical trade-off where bounding one parameter (the narrow width) causes the other parameter (the size) to grow above its worst case. The size lower bound is super-exponential in the formula size and improves a related supercritical trade-off by Razborov [Alexander A. Razborov, 2016]. To prove our result, we develop a new variant of the k-pebble EF-game for FO^k to reason about tree-like refutation size in a similar way as the Prover-Delayer games in proof complexity. We analyze this game on the compressed CFI graphs introduced by Grohe, Lichter, Neuen, and Schweitzer [Martin Grohe et al., 2023]. Using a recent improved robust compressed CFI construction of de Rezende, Fleming, Janett, Nordström, and Pang [Susanna F. de Rezende et al., 2024], we obtain a similar bound for width k (instead of the stronger but less common narrow width) and make the result more robust.

Cite As Get BibTex

Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical Size-Width Tree-Like Resolution Trade-Offs for Graph Isomorphism. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.18

Author Details

Christoph Berkholz
  • Technische Universität Ilmenau, Germany
Moritz Lichter
  • RWTH Aachen University, Germany
Harry Vinall-Smeeth
  • Technische Universität Ilmenau, Germany

Funding

Christoph Berkholz and Harry Vinall-Smeeth: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 414325841.
  • Lichter, Moritz: Funded by the European Union (ERC, SymSim, 101054974). Views and opinions expressed are those of the author(s) and do not necessarily reflect those of the European Union or the ERC. Neither the European Union nor the granting authority can be held responsible for them.

References

  1. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. URL: https://doi.org/10.1016/J.JCSS.2007.06.025.
  2. Albert Atserias, Meena Mahajan, Jakob Nordström, and Alexander Razborov. Proof complexity and beyond. Oberwolfach Report, 2024. Workshop held 24-29 March 2024. URL: https://doi.org/10.14760/OWR-2024-15.
  3. Albert Atserias and Elitza N. Maneva. Sherali-Adams relaxations and indistinguishability in counting logics. SIAM J. Comput., 42(1):112-137, 2013. URL: https://doi.org/10.1137/120867834.
  4. László Babai. Graph isomorphism in quasipolynomial time [extended abstract]. In 48th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2016, Cambridge, MA, USA, June 18-21, 2016, pages 684-697. ACM, 2016. URL: https://doi.org/10.1145/2897518.2897542.
  5. Paul Beame, Chris Beck, and Russell Impagliazzo. Time-space trade-offs in resolution: Superpolynomial lower bounds for superlinear space. SIAM J. Comput., 45(4):1612-1645, 2016. URL: https://doi.org/10.1137/130914085.
  6. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 813-822. ACM, 2013. URL: https://doi.org/10.1145/2488608.2488711.
  7. Eli Ben-Sasson, Russell Impagliazzo, and Avi Wigderson. Near optimal separation of tree-like and general resolution. Comb., 24(4):585-603, 2004. URL: https://doi.org/10.1007/S00493-004-0036-5.
  8. Eli Ben-Sasson and Jakob Nordström. Short proofs may be spacious: An optimal separation of space and length in resolution. In 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA, pages 709-718. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/FOCS.2008.42.
  9. Eli Ben-Sasson and Jakob Nordström. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Innovations in Computer Science - ICS 2011, Tsinghua University, Beijing, China, January 7-9, 2011. Proceedings, pages 401-416. Tsinghua University Press, 2011. URL: http://conference.iiis.tsinghua.edu.cn/ICS2011/content/papers/3.html.
  10. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. In Proceedings of the Thirty-First Annual ACM Symposium on Theory of Computing, May 1-4, 1999, Atlanta, Georgia, USA, pages 517-526. ACM, 1999. URL: https://doi.org/10.1145/301250.301392.
  11. Christoph Berkholz. On the complexity of finding narrow proofs. In 53rd Annual IEEE Symposium on Foundations of Computer Science, FOCS 2012, New Brunswick, NJ, USA, October 20-23, 2012, pages 351-360. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/FOCS.2012.48.
  12. Christoph Berkholz and Martin Grohe. Limitations of algebraic approaches to graph isomorphism testing. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part I, volume 9134 of Lecture Notes in Computer Science, pages 155-166. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47672-7_13.
  13. Christoph Berkholz and Martin Grohe. Linear diophantine equations, group CSPs, and graph isomorphism. In Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2017, Barcelona, Spain, Hotel Porta Fira, January 16-19, pages 327-339. SIAM, 2017. URL: https://doi.org/10.1137/1.9781611974782.21.
  14. Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical size-width tree-like resolution trade-offs for graph isomorphism. CoRR, 2024. arXiv preprint. URL: https://doi.org/10.48550/arXiv.2407.17947.
  15. Christoph Berkholz and Jakob Nordström. Near-optimal lower bounds on quantifier depth and Weisfeiler-Leman refinement steps. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, July 5-8, 2016, pages 267-276, 2016. URL: https://doi.org/10.1145/2933575.2934560.
  16. Christoph Berkholz and Jakob Nordström. Supercritical space-width trade-offs for resolution. SIAM J. Comput., 49(1):98-118, 2020. URL: https://doi.org/10.1137/16M1109072.
  17. Jin-yi Cai, Martin Fürer, and Neil Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12(4):389-410, 1992. URL: https://doi.org/10.1007/BF01305232.
  18. Anuj Dawar, Erich Grädel, and Moritz Lichter. Limitations of the invertible-map equivalences. J. Log. Comput., September 2022. URL: https://doi.org/10.1093/logcom/exac058.
  19. Susanna F. de Rezende, Noah Fleming, Duri Andrea Janett, Jakob Nordström, and Shuo Pang. Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and Weisfeiler-Leman. CoRR, abs/2411.14267, 2024. arXiv preprint. URL: https://doi.org/10.48550/arXiv.2411.14267.
  20. Martin Fürer. Weisfeiler-Lehman refinement requires at least a linear number of iterations. In 28th International Colloquium on Automata, Languages, and Programming, ICALP 2001, Crete, Greece, July 8-12, 2001, Proceedings, volume 2076 of Lecture Notes in Computer Science, pages 322-333. Springer, 2001. URL: https://doi.org/10.1007/3-540-48224-5_27.
  21. Nicola Galesi and Neil Thapen. Resolution and pebbling games. In Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 76-90. Springer, 2005. URL: https://doi.org/10.1007/11499107_6.
  22. Erich Grädel, Martin Grohe, Benedikt Pago, and Wied Pakusa. A finite-model-theoretic view on propositional proof complexity. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:4)2019.
  23. Martin Grohe. Fixed-point definability and polynomial time on graphs with excluded minors. J. ACM, 59(5):27:1-27:64, 2012. URL: https://doi.org/10.1145/2371656.2371662.
  24. Martin Grohe, Moritz Lichter, and Daniel Neuen. The iteration number of the Weisfeiler-Leman algorithm. ACM Trans. Comput. Log., 26(1):6:1-6:31, 2025. URL: https://doi.org/10.1145/3708891.
  25. Martin Grohe, Moritz Lichter, Daniel Neuen, and Pascal Schweitzer. Compressing CFI graphs and lower bounds for the Weisfeiler-Leman refinements. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023, pages 798-809. IEEE, 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00052.
  26. Martin Grohe and Daniel Neuen. Recent advances on the graph isomorphism problem. In Surveys in Combinatorics, 2021: Invited lectures from the 28th British Combinatorial Conference, Durham, UK, July 5-9, 2021, pages 187-234. Cambridge University Press, 2021. URL: https://doi.org/10.1017/9781009036214.006.
  27. Martin Grohe and Daniel Neuen. Isomorphism for tournaments of small twin width. In 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia, volume 297 of LIPIcs, pages 78:1-78:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.ICALP.2024.78.
  28. Martin Grohe and Martin Otto. Pebble games and linear equations. J. Symb. Log., 80(3):797-844, 2015. URL: https://doi.org/10.1017/JSL.2015.28.
  29. Neil Immerman. Upper and lower bounds for first order expressibility. J. Comput. Syst. Sci., 25(1):76-98, 1982. URL: https://doi.org/10.1016/0022-0000(82)90011-3.
  30. Richard M. Karp. Reducibility among combinatorial problems. In Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA, The IBM Research Symposia Series, pages 85-103. Plenum Press, New York, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  31. Moritz Lichter. Witnessed symmetric choice and interpretations in fixed-point logic with counting. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023), volume 261 of LIPIcs, pages 133:1-133:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ICALP.2023.133.
  32. 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 Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2014, Portland, Oregon, USA, January 5-7, 2014, pages 1659-1677. SIAM, 2014. URL: https://doi.org/10.1137/1.9781611973402.120.
  33. Benedikt Pago. Finite model theory and proof complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the extended polynomial calculus. In 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, volume 252 of LIPIcs, pages 31:1-31:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CSL.2023.31.
  34. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-SAT (preliminary version). In Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9-11, 2000, San Francisco, CA, USA, pages 128-136. ACM/SIAM, 2000. URL: http://dl.acm.org/citation.cfm?id=338219.338244.
  35. Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1-16:14, 2016. URL: https://doi.org/10.1145/2858790.
  36. Pascal Schweitzer and Constantin Seebach. Resolution with symmetry rule applied to linear equations. In 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, March 16-19, 2021, Saarbrücken, Germany (Virtual Conference), volume 187 of LIPIcs, pages 58:1-58:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.STACS.2021.58.
  37. Paul D. Seymour and Robin Thomas. Graph searching and a min-max theorem for tree-width. J. Comb. Theory, Ser. B, 58(1):22-33, 1993. URL: https://doi.org/10.1006/jctb.1993.1027.
  38. Neil Thapen. A tradeoff between length and width in resolution. Theory Comput., 12(1):1-14, 2016. URL: https://doi.org/10.4086/TOC.2016.V012A005.
  39. Jacobo Torán. On the hardness of graph isomorphism. SIAM J. Comput., 33(5):1093-1108, 2004. URL: https://doi.org/10.1137/S009753970241096X.
  40. Jacobo Torán. On the resolution complexity of graph non-isomorphism. In Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, volume 7962 of Lecture Notes in Computer Science, pages 52-66. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_6.
  41. 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, July 4-8, 2023, Alghero, Italy, volume 271 of LIPIcs, pages 26:1-26:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.SAT.2023.26.
  42. Jacobo Torán and Florian Wörz. Number of variables for graph differentiation and the resolution of graph isomorphism formulas. ACM Trans. Comput. Log., 24(3):23:1-23:25, 2023. URL: https://doi.org/10.1145/3580478.
  43. Alasdair Urquhart. The depth of resolution proofs. Stud Logica, 99(1-3):349-364, 2011. URL: https://doi.org/10.1007/S11225-011-9356-9.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact