First-Order Logic with Connectivity Operators
First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates conn_k(x,y,z_1,…,z_k) that hold true in a graph if there exists a path between (the valuations of) x and y after (the valuations of) z_1,…,z_k have been deleted, we obtain separator logic FO+conn. We show that separator logic can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes. Denote by FO+conn_k the fragment of separator logic that is restricted to connectivity predicates with at most k+2 variables (that is, at most k deletions). We show that FO+conn_{k+1} is strictly more expressive than FO+conn_k for all k ≥ 0. We then study the limitations of separator logic and prove that it cannot express planarity, and, in particular, not the disjoint paths problem. We obtain the stronger disjoint-paths logic FO+DP by adding the atomic predicates disjoint-paths_k[(x_1,y_1),…,(x_k,y_k)] that evaluate to true if there are internally vertex-disjoint paths between (the valuations of) x_i and y_i for all 1 ≤ i ≤ k. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Again we show that the fragments FO+DP_k that use predicates for at most k disjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitive-closure logics and monadic second-order logic.
First-order logic
graph theory
connectivity
Theory of computation~Finite Model Theory
Mathematics of computing~Combinatorics
34:1-34:17
Regular Paper
This paper is a part of the ANR-DFG project Unifying Theories for Multivariate Algorithms (UTMA), which has received funding from the German Research Foundation (DFG) with grant agreement No 446200270.
We thank Mikołaj Bojańczyk for fruitful discussions. He independently studied FO+conn and suggested the name separator logic for this logic. We also thank Michał Pilipczuk and Szymon Toruńczyk for fruitful discussions.
Nicole
Schirrmacher
Nicole Schirrmacher
University of Bremen, Germany
https://orcid.org/0000-0002-1740-7478
Sebastian
Siebertz
Sebastian Siebertz
University of Bremen, Germany
https://orcid.org/0000-0002-6347-1198
Alexandre
Vigny
Alexandre Vigny
University of Bremen, Germany
https://orcid.org/0000-0002-4298-8876
10.4230/LIPIcs.CSL.2022.34
Akanksha Agrawal, Lawqueen Kanesh, Fahad Panolan, M. S. Ramanujan, and Saket Saurabh. An FPT algorithm for elimination distance to bounded degree graphs. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021.
Mikołaj Bojańczyk. Separator logic and star-free expressions for graphs. arXiv preprint, 2021. URL: http://arxiv.org/abs/2107.13953.
http://arxiv.org/abs/2107.13953
Édouard Bonnet, Ugo Giocanti, Patrice Ossona de Mendez, Pierre Simon, Stéphan Thomassé, and Szymon Toruńczyk. Twin-width IV: ordered graphs and matrices. arXiv preprint, 2021. URL: http://arxiv.org/abs/2102.03117.
http://arxiv.org/abs/2102.03117
Jannis Bulian. Parameterized complexity of distances to sparse graph classes. Technical report, University of Cambridge, Computer Laboratory, 2017.
Jannis Bulian and Anuj Dawar. Graph isomorphism parameterized by elimination distance to bounded degree. Algorithmica, 75(2):363-382, 2016.
Michael Buro. Simple amazons endgames and their connection to Hamilton circuits in cubic subgrid graphs. In International Conference on Computers and Games, pages 250-261. Springer, 2000.
Bruno Courcelle. The monadic second-order logic of graphs. I. recognizable sets of finite graphs. Information and computation, 85(1):12-75, 1990.
Bruno Courcelle, Johann A. Makowsky, and Udi Rotics. Linear time solvable optimization problems on graphs of bounded clique-width. Theory of Computing Systems, 33(2):125-150, 2000.
Marek Cygan, Fedor V. Fomin, Lukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Parameterized Algorithms. Springer, 2015.
Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Springer Science & Business Media, 2005.
Ronald Fagin. Generalized first-order spectra and polynomial-time recognizable sets. Complexity of computation, 7:43-73, 1974.
Fedor V. Fomin, Petr A. Golovach, Giannos Stamoulis, and Dimitrios M. Thilikos. An algorithmic meta-theorem for graph modification to planarity and FOL. In 28th Annual European Symposium on Algorithms, ESA 2020, pages 51:1-51:17, 2020.
Fedor V. Fomin, Petr A. Golovach, and Dimitrios M. Thilikos. Parameterized complexity of elimination distance to first-order logic properties. arXiv preprint, 2021. URL: http://arxiv.org/abs/2104.02998.
http://arxiv.org/abs/2104.02998
Fedor V. Fomin, Daniel Lokshtanov, Fahad Panolan, Saket Saurabh, and Meirav Zehavi. Hitting topological minors is FPT. In Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, pages 1317-1326, 2020.
Robert Ganian, Petr Hliněnỳ, Alexander Langer, Jan Obdržálek, Peter Rossmanith, and Somnath Sikdar. Lower bounds on the complexity of MSO1 model-checking. Journal of Computer and System Sciences, 80(1):180-194, 2014.
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. Springer Science & Business Media, 2007.
Martin Grohe. Logic, graphs, and algorithms. Logic and automata, 2:357-422, 2008.
Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. Journal of the ACM (JACM), 64(3):17, 2017.
Eva-Maria C. Hols, Stefan Kratsch, and Astrid Pieterse. Elimination distances, blocking sets, and kernels for vertex cover. In STACS, 2020.
Bart M. P. Jansen, Jari J. H. de Kroon, and Michał Włodarczyk. Vertex deletion parameterized by elimination distance and even less. In Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing, pages 1757-1769, 2021.
Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second-order logic. In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 189-198. IEEE, 2010.
Leonid Libkin. Elements of finite model theory. Springer Science & Business Media, 2013.
Alexander Lindermayr, Sebastian Siebertz, and Alexandre Vigny. Elimination distance to bounded degree on planar graphs. In 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, August 24-28, 2020, Prague, Czech Republic, pages 65:1-65:12, 2020.
Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and data structures for first-order logic with connectivity under vertex failures. arXiv preprint, 2021. URL: http://arxiv.org/abs/2111.03725.
http://arxiv.org/abs/2111.03725
Bruce Reed, Kaleigh Smith, and Adrian Vetta. Finding odd cycle transversals. Operations Research Letters, 32(4):299-301, 2004.
Neil Robertson and P. D. Seymour. Graph minors. XIII. the disjoint paths problem. J. Combin. Theory Ser. B, 63:65-110, 1995.
Wolfgang Thomas. Languages, automata, and logic. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages, Volume 3: Beyond Words, pages 389-455. Springer, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_7.
https://doi.org/10.1007/978-3-642-59126-6_7
Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode