Document Open Access Logo

Finite Model Theory and Proof Complexity Revisited: Distinguishing Graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus

Author Benedikt Pago

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2023.31.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
Keywords
  • finite model theory
  • proof complexity
  • graph isomorphism

Metrics

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

Abstract

This paper extends prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards better understanding the limits of CPT. A super-polynomial EPC lower bound for a Ptime-instance of the graph isomorphism problem would separate CPT from Ptime and thus solve a major open question in finite model theory. Further, using our result, we provide a model theoretic proof for the separation of bounded-degree polynomial calculus and bounded-degree extended polynomial calculus.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.31

Author Details

Benedikt Pago
  • Mathematical Foundations of Computer Science, RWTH Aachen University, Germany

Acknowledgements

I would like to thank Daniel Wiebking for extensively answering my numerous questions on Deep Weisfeiler Leman and the properties of coherent configurations.

References

  1. Faried Abu Zaid, Erich Grädel, Martin Grohe, and Wied Pakusa. Choiceless Polynomial Time on structures with small Abelian colour classes. In Mathematical Foundations of Computer Science 2014, volume 8634 of Lecture Notes in Computer Science, pages 50-62. Springer, 2014. URL: http://logic.rwth-aachen.de/pub/pakusa/cptcan.pdf.
  2. Yaroslav Alekseev. A Lower Bound for Polynomial Calculus with Extension Rule. In Valentine Kabanets, editor, 36th Computational Complexity Conference (CCC 2021), volume 200 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.21.
  3. Christoph Berkholz and Martin Grohe. Limitations of algebraic approaches to graph isomorphism testing. In International Colloquium on Automata, Languages, and Programming, pages 155-166. Springer, 2015. Google Scholar
  4. Andreas Blass, Yuri Gurevich, and Saharon Shelah. Choiceless polynomial time. Annals of Pure and Applied Logic, 100(1-3):141-187, 1999. Google Scholar
  5. J. Cai, M. Fürer, and N. Immerman. An optimal lower bound on the number of variables for graph identification. Combinatorica, 12:389-410, 1992. Google Scholar
  6. Ashok K Chandra and David Harel. Structure and complexity of relational queries. In 21st Annual Symposium on Foundations of Computer Science (sfcs 1980), pages 333-347. IEEE, 1980. URL: https://doi.org/10.1109/SFCS.1980.41.
  7. Gang Chen and Ilia Ponomarenko. Lectures on coherent configurations. Lecture notes, 2019. Available at URL: http://www.pdmi.ras.ru/~inp/ccNOTES.pdf.
  8. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 174-183, 1996. Google Scholar
  9. Anuj Dawar. The nature and power of fixed-point logic with counting. ACM SIGLOG News, 2(1):8-21, 2015. Google Scholar
  10. Anuj Dawar, David Richerby, and Benjamin Rossman. Choiceless polynomial time, counting and the Cai-Fürer-Immerman graphs. Annals of Pure and Applied Logic, 152(1-3):31-50, 2008. Google Scholar
  11. Susanna F de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The power of negative reasoning. In 36th Computational Complexity Conference (CCC 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  12. E. Grädel, W. Pakusa, S. Schalthöfer, and L. Kaiser. Characterising choiceless polynomial time with first-order interpretations. In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 677-688, 2015. Google Scholar
  13. Erich Grädel and Martin Grohe. Is polynomial time choiceless? In Fields of Logic and Computation II, pages 193-209. Springer, 2015. Google Scholar
  14. Erich Grädel, Martin Grohe, Benedikt Pago, and Wied Pakusa. A finite-model-theoretic view on propositional proof complexity. Logical Methods in Computer Science, 15, 2019. Google Scholar
  15. Martin Grohe. The quest for a logic capturing PTIME. In 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pages 267-271. IEEE, 2008. URL: https://doi.org/10.1109/LICS.2008.11.
  16. Martin Grohe, Pascal Schweitzer, and Daniel Wiebking. Deep Weisfeiler Leman, 2020. URL: http://arxiv.org/abs/2003.10935.
  17. Yuri Gurevich. Logic and the Challenge of Computer Science. In Current Trends in Theoretical Computer Science. Computer Science Press, 1988. Google Scholar
  18. Yuri Gurevich and Saharon Shelah. On finite rigid structures. The Journal of Symbolic Logic, 61(2):549-562, 1996. Google Scholar
  19. Lauri Hella. Logical hierarchies in PTIME. Information and Computation, 129(1):1-19, 1996. Google Scholar
  20. Neil Immerman and Eric Lander. Describing graphs: A first-order approach to graph canonization. In Complexity theory retrospective, pages 59-81. Springer, 1990. Google Scholar
  21. Sandra Kiefer. The Weisfeiler-Leman algorithm: an exploration of its power. ACM SIGLOG News, 7(3):5-27, 2020. Google Scholar
  22. Moritz Lichter. Separating rank logic from polynomial time. CoRR, abs/2104.12999, 2021. URL: http://arxiv.org/abs/2104.12999.
  23. Benedikt Pago. Choiceless Computation and Symmetry: Limitations of Definability. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1-33:21, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.33.
  24. Benedikt Pago. Finite model theory and proof complexity revisited: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus. arXiv, 2022. URL: http://arxiv.org/abs/2206.05086.
  25. Wied Pakusa. Linear Equation Systems and the Search for a Logical Characterisation of Polynomial Time. PhD thesis, RWTH Aachen, 2015. Google Scholar
  26. Benjamin Rossman. Choiceless computation and symmetry. In Fields of logic and computation, pages 565-580. Springer, 2010. Google Scholar
  27. Svenja Schalthöfer. Choiceless Computation and Logic. PhD thesis, RWTH Aachen, 2020. Google Scholar
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