Document Open Access Logo

Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting

Author Moritz Lichter

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2023.133.pdf
  • Filesize: 0.81 MB
  • 20 pages

Document Identifiers

Author Details

Moritz Lichter
  • TU Darmstadt, Germany

Funding

This work received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (EngageS: agreement No. 820148).

Cite As Get BibTex

Moritz Lichter. Witnessed Symmetric Choice and Interpretations in Fixed-Point Logic with Counting. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 133:1-133:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ICALP.2023.133

Abstract

At the core of the quest for a logic for Ptime is a mismatch between algorithms making arbitrary choices and isomorphism-invariant logics. One approach to tackle this problem is witnessed symmetric choice. It allows for choices from definable orbits certified by definable witnessing automorphisms.
We consider the extension of fixed-point logic with counting (IFPC) with witnessed symmetric choice (IFPC+WSC) and a further extension with an interpretation operator (IFPC+WSC+I). The latter operator evaluates a subformula in the structure defined by an interpretation. When similarly extending pure fixed-point logic (IFP), IFP+WSC+I simulates counting which IFP+WSC fails to do. For IFPC+WSC, it is unknown whether the interpretation operator increases expressiveness and thus allows studying the relation between WSC and interpretations beyond counting.
In this paper, we separate IFPC+WSC from IFPC+WSC+I by showing that IFPC+WSC is not closed under FO-interpretations. By the same argument, we answer an open question of Dawar and Richerby regarding non-witnessed symmetric choice in IFP. Additionally, we prove that nesting WSC-operators increases the expressiveness using the so-called CFI graphs. We show that if IFPC+WSC+I canonizes a particular class of base graphs, then it also canonizes the corresponding CFI graphs. This differs from various other logics, where CFI graphs provide difficult instances.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Complexity theory and logic
Keywords
  • witnessed symmetric choice
  • interpretation
  • fixed-point logic
  • counting
  • CFI graphs
  • logic for PTime

Metrics

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

Related Versions

References

  1. Markus Anders and Pascal Schweitzer. Search problems in trees with symmetries: Near optimal traversal strategies for individualization-refinement algorithms. In 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 16:1-16:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.16.
  2. Vikraman Arvind and Somenath Biswas. Expressibility of first order logic with a nondeterministic inductive operator. In STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, volume 247 of Lecture Notes in Computer Science, pages 323-335. Springer, 1987. URL: https://doi.org/10.1007/BFb0039616.
  3. Andreas Blass and Yuri Gurevich. The logic of choice. J. Symb. Log., 65(3):1264-1310, 2000. URL: https://doi.org/10.2307/2586700.
  4. Andreas Blass, Yuri Gurevich, and Saharon Shelah. On polynomial time computation over unordered structures. J. Symb. Log., 67(3):1093-1125, 2002. URL: https://doi.org/10.2178/jsl/1190150152.
  5. 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.
  6. Ashok K. Chandra and David Harel. Structure and complexity of relational queries. J. Comput. Syst. Sci., 25(1):99-128, 1982. URL: https://doi.org/10.1016/0022-0000(82)90012-5.
  7. Anuj Dawar, Erich Grädel, and Moritz Lichter. Limitations of the invertible-map equivalences. J. Log. Comput., 2022. URL: https://doi.org/10.1093/logcom/exac058.
  8. Anuj Dawar and Kashif Khan. Constructing hard examples for graph isomorphism. J. Graph Algorithms Appl., 23(2):293-316, 2019. URL: https://doi.org/10.7155/jgaa.00492.
  9. Anuj Dawar and David Richerby. A fixed-point logic with symmetric choice. In Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, pages 169-182. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_16.
  10. Anuj Dawar and David Richerby. Fixed-point logics with nondeterministic choice. J. Log. Comput., 13(4):503-530, 2003. URL: https://doi.org/10.1093/logcom/13.4.503.
  11. Anuj Dawar and David Richerby. The power of counting logics on restricted classes of finite structures. In Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 84-98. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_10.
  12. Anuj Dawar, David Richerby, and Benjamin Rossman. Choiceless Polynomial Time, counting and the Cai-Fürer-Immerman graphs. Ann. Pure Appl. Logic, 152(1-3):31-50, 2008. URL: https://doi.org/10.1016/j.apal.2007.11.011.
  13. Heinz-Dieter Ebbinghaus. Extended logics: the general framework. In Model-Theoretic Logics, Perspectives in MathematicalLogic, pages 25-76. Association for Symbolic Logic, 1985. Google Scholar
  14. Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. In Complexity of computation (Proc. SIAM-AMS Sympos. Appl. Math., New York, 1973), pages 43-73. SIAM-AMS Proc., Vol. VII, 1974. Google Scholar
  15. Françoise Gire and H. Khanh Hoang. An extension of fixpoint logic with a symmetry-based choice construct. Inf. Comput., 144(1):40-65, 1998. URL: https://doi.org/10.1006/inco.1998.2712.
  16. Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg, 2007. URL: https://doi.org/10.1007/3-540-68804-8.
  17. Erich Grädel and Wied Pakusa. Rank logic is dead, long live rank logic! J. Symb. Log., 84(1):54-87, 2019. URL: https://doi.org/10.1017/jsl.2018.33.
  18. Erich Grädel, Wied Pakusa, Svenja Schalthöfer, and Lukasz Kaiser. Characterising Choiceless Polynomial Time with first-order interpretations. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 677-688. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.68.
  19. Martin Grohe. The quest for a logic capturing PTIME. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 267-271. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.11.
  20. Martin Grohe. Descriptive Complexity, Canonization, and Definable Graph Structure Theory. Cambridge University Press, 2017. Google Scholar
  21. Martin Grohe and Daniel Neuen. Canonisation and definability for graphs of bounded rank width. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-13. IEEE Computer Society, 2019. URL: https://doi.org/10.1109/LICS.2019.8785682.
  22. Yuri Gurevich. Logic and the challenge of computer science. In Current Trends in Theoretical Computer Science, pages 1-57. Computer Science Press, 1988. Google Scholar
  23. Yuri Gurevich. From invariants to canonization. Bull. EATCS, 63, 1997. Google Scholar
  24. Yuri Gurevich and Saharon Shelah. On finite rigid structures. J. Symb. Log., 61(2):549-562, 1996. URL: https://doi.org/10.2307/2275675.
  25. Lauri Hella. Logical hierarchies in PTIME. Information and Computation, 129(1):1-19, 1996. URL: https://doi.org/10.1006/inco.1996.0070.
  26. Neil Immerman. Expressibility as a complexity measure: results and directions. In Proceedings of the Second Annual Conference on Structure in Complexity Theory, Cornell University, Ithaca, New York, USA, June 16-19, 1987. IEEE Computer Society, 1987. Google Scholar
  27. Neil Immerman. Languages that capture complexity classes. SIAM J. Comput., 16(4):760-778, 1987. URL: https://doi.org/10.1137/0216051.
  28. Sandra Kiefer, Pascal Schweitzer, and Erkal Selman. Graphs identified by logics with counting. In Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I, volume 9234 of Lecture Notes in Computer Science, pages 319-330. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_25.
  29. Moritz Lichter. Separating rank logic from polynomial time. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE Computer Society, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470598.
  30. Moritz Lichter. Witnessed symmetric choice and interpretations in fixed-point logic with counting. CoRR, abs/2210.07869, 2022. arXiv preprint. URL: https://doi.org/10.48550/arXiv.2210.07869.
  31. Moritz Lichter and Pascal Schweitzer. Canonization for bounded and dihedral color classes in Choiceless Polynomial Time. In 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 31:1-31:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.31.
  32. Moritz Lichter and Pascal Schweitzer. Choiceless Polynomial Time with witnessed symmetric choice. In LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2-5, 2022, pages 30:1-30:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533348.
  33. Rudolf Mathon. A note on the graph isomorphism counting problem. Inf. Process. Lett., 8(3):131-132, 1979. URL: https://doi.org/10.1016/0020-0190(79)90004-8.
  34. 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 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 138-150. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188900.
  35. Martin Otto. Bounded variable logics and counting - A study in finite models, volume 9 of Lecture Notes in Logic. Springer, 1997. Google Scholar
  36. Martin Otto. Epsilon-logic is more expressive than first-order logic over finite structures. J. Symb. Log., 65(4):1749-1757, 2000. URL: https://doi.org/10.2307/2695073.
  37. Wied Pakusa, Svenja Schalthöfer, and Erkal Selman. Definability of Cai-Fürer-Immerman problems in Choiceless Polynomial Time. In 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 19:1-19:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.19.
  38. David Richerby. Fixed-point logics with choice. PhD thesis, University of Cambridge, 2004. Google Scholar
  39. 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.
  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. Number of variables for graph differentiation and the resolution of GI formulas. In 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 36:1-36:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CSL.2022.36.
  42. 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 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I, volume 8634 of Lecture Notes in Computer Science, pages 50-62. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_5.
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 About DROPS Imprint Privacy Contact