Document Open Access Logo

Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures

Authors Michał Pilipczuk , Nicole Schirrmacher , Sebastian Siebertz , Szymon Toruńczyk , Alexandre Vigny

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.102.pdf
  • Filesize: 0.99 MB
  • 18 pages

Document Identifiers

Author Details

Michał Pilipczuk
  • University of Warsaw, Poland
Nicole Schirrmacher
  • Universität Bremen, Germany
Sebastian Siebertz
  • Universität Bremen, Germany
Szymon Toruńczyk
  • University of Warsaw, Poland
Alexandre Vigny
  • Universität Bremen, Germany

Funding

This paper is a part of project BOBR that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 948057) and part of the French-German Collaboration ANR/DFG Project UTMA supported by the German Research Foundation (DFG) through grant agreement No 446200270.

Acknowledgements

We thank Ismaël Jecker, Pierre Ohlmann and Wojciech Przybyszewski for useful discussions. In particular, Wojciech Przybyszewski showed how to improve the dependency on k in the running time from double exponential to single exponential in Theorem 1.1 (see Theorem 2.4).

Cite As Get BibTex

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. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 102:1-102:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ICALP.2022.102

Abstract

We introduce a new data structure for answering connectivity queries in undirected graphs subject to batched vertex failures. Precisely, given any graph G and integer parameter k, we can in fixed-parameter time construct a data structure that can later be used to answer queries of the form: "are vertices s and t connected via a path that avoids vertices u₁,…, u_k?" in time 2^𝒪(k). In the terminology of the literature on data structures, this gives the first deterministic data structure for connectivity under vertex failures where for every fixed number of failures, all operations can be performed in constant time.
With the aim to understand the power and the limitations of our new techniques, we prove an algorithmic meta theorem for the recently introduced separator logic, which extends first-order logic with atoms for connectivity under vertex failures. We prove that the model-checking problem for separator logic is fixed-parameter tractable on every class of graphs that exclude a fixed topological minor. We also show a weak converse. This implies that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor.
The backbone of our proof relies on a decomposition theorem of Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [SICOMP '19], which provides a tree decomposition of a given graph into bags that are unbreakable. Crucially, unbreakability allows to reduce separator logic to plain first-order logic within each bag individually. Guided by this observation, we design our model-checking algorithm using dynamic programming over the tree decomposition, where the transition at each bag amounts to running a suitable model-checking subprocedure for plain first-order logic. This approach is robust enough to provide also an extension to efficient enumeration of answers to a query expressed in separator logic.

Subject Classification

ACM Subject Classification
  • Theory of computation → Fixed parameter tractability
  • Theory of computation → Finite Model Theory
  • Mathematics of computing → Graph algorithms
Keywords
  • Combinatorics and graph theory
  • Computational applications of logic
  • Data structures
  • Fixed-parameter algorithms and complexity
  • Graph algorithms

Metrics

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

Related Versions

References

  1. Akanksha Agrawal, Lawqueen Kanesh, Daniel Lokshtanov, Fahad Panolan, MS Ramanujan, Saket Saurabh, and Meirav Zehavi. Deleting, eliminating and decomposing to hereditary classes are all fpt-equivalent. In Proceedings of the 2022 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1976-2004. SIAM, 2022. Google Scholar
  2. Akanksha Agrawal, Lawqueen Kanesh, Fahad Panolan, M. S. Ramanujan, and Saket Saurabh. An FPT algorithm for elimination distance to bounded degree graphs. In Proceedings of the 38th International Symposium on Theoretical Aspects of Computer Science, STACS 2021, volume 187 of LIPIcs, pages 5:1-5:11. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  3. Akanksha Agrawal, Lawqueen Kanesh, Fahad Panolan, MS 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. Google Scholar
  4. Antoine Amarilli, Pierre Bourhis, Stefan Mengel, and Matthias Niewerth. Enumeration on trees with tractable combined complexity and efficient updates. In Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2019, pages 89-103. ACM, 2019. Google Scholar
  5. Guillaume Bagan. MSO queries on tree decomposable structures are computable with linear delay. In Proceedings of the 15th International Conference on Computer Science Logic, CSL 2006, volume 4207 of Lecture Notes in Computer Science, pages 167-181. Springer, 2006. URL: https://doi.org/10.1007/11874683_11.
  6. Mikołaj Bojańczyk. Separator logic and star-free expressions for graphs. CoRR, abs/2107.13953, 2021. URL: http://arxiv.org/abs/2107.13953.
  7. Mikołaj Bojańczyk and Michał Pilipczuk. Definability equals recognizability for graphs of bounded treewidth. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pages 407-416. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934508.
  8. Glencora Borradaile, Seth Pettie, and Christian Wulff-Nilsen. Connectivity oracles for planar graphs. In Scandinavian Workshop on Algorithm Theory, pages 316-327. Springer, 2012. Google Scholar
  9. Jannis Bulian and Anuj Dawar. Graph isomorphism parameterized by elimination distance to bounded degree. Algorithmica, 75(2):363-382, 2016. Google Scholar
  10. Jannis Bulian and Anuj Dawar. Fixed-parameter tractable distances to sparse graph classes. Algorithmica, 79(1):139-158, 2017. Google Scholar
  11. Rajesh Chitnis, Marek Cygan, MohammadTaghi Hajiaghayi, Marcin Pilipczuk, and Michał Pilipczuk. Designing FPT algorithms for cut problems using randomized contractions. SIAM Journal on Computing, 45(4):1171-1229, 2016. URL: https://doi.org/10.1137/15M1032077.
  12. Thomas Colcombet. A combinatorial theorem for trees. In Proceedings of the 34th International Colloquium Automata, Languages and Programming, ICALP 2007, volume 4596 of Lecture Notes in Computer Science, pages 901-912. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_77.
  13. Bruno Courcelle. The Monadic Second-Order logic of graphs. I. Recognizable sets of finite graphs. Information and Computation, 85(1):12-75, 1990. URL: https://doi.org/10.1016/0890-5401(90)90043-H.
  14. Marek Cygan, Paweł Komosa, Daniel Lokshtanov, Marcin Pilipczuk, Michał Pilipczuk, Saket Saurabh, and Magnus Wahlström. Randomized contractions meet lean decompositions. ACM Transactions on Algorithms, 17(1):6:1-6:30, 2021. URL: https://doi.org/10.1145/3426738.
  15. Marek Cygan, Daniel Lokshtanov, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Minimum Bisection is fixed-parameter tractable. SIAM Journal on Computing, 48(2):417-450, 2019. URL: https://doi.org/10.1137/140988553.
  16. Ran Duan and Seth Pettie. Connectivity oracles for failure prone graphs. In Proceedings of the 42nd ACM Symposium on Theory of Computing, STOC 2010, pages 465-474. ACM, 2010. URL: https://doi.org/10.1145/1806689.1806754.
  17. Ran Duan and Seth Pettie. Connectivity oracles for graphs subject to vertex failures. SIAM Journal on Computing, 49(6):1363-1396, 2020. URL: https://doi.org/10.1137/17M1146610.
  18. Arnaud Durand, Nicole Schweikardt, and Luc Segoufin. Enumerating answers to first-order queries over databases of low degree. In Proceedings of the 33rd ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pages 121-131, 2014. Google Scholar
  19. Zdeněk Dvořák, Daniel Král, and Robin Thomas. Testing first-order properties for subclasses of sparse graphs. Journal of the ACM, 60(5):36:1-36:24, 2013. URL: https://doi.org/10.1145/2499483.
  20. Fedor V Fomin, Petr A Golovach, Ignasi Sau, Giannos Stamoulis, and Dimitrios M Thilikos. A compound logic for modification problems: Big kingdoms fall from within. arXiv preprint, 2021. URL: http://arxiv.org/abs/2111.02755.
  21. Fedor V. Fomin, Petr A. Golovach, and Dimitrios M. Thilikos. Parameterized complexity of elimination distance to first-order logic properties. In Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1-13. IEEE, 2021. Google Scholar
  22. Daniele Frigioni and Giuseppe F. Italiano. Dynamically switching vertices in planar graphs. In Proceedings of the 5th Annual European Symposium on Algorithms, ESA 1997, volume 1284 of Lecture Notes in Computer Science, pages 186-199. Springer, 1997. Google Scholar
  23. 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. Google Scholar
  24. Martin Grohe, Stephan Kreutzer, and Sebastian Siebertz. Deciding first-order properties of nowhere dense graphs. Journal of the ACM, 64(3):17:1-17:32, 2017. URL: https://doi.org/10.1145/3051095.
  25. Dov Harel and Robert Endre Tarjan. Fast algorithms for finding nearest common ancestors. SIAM Journal on Computing, 13(2):338-355, 1984. URL: https://doi.org/10.1137/0213024.
  26. Bart M. P. Jansen and Jari J. H. de Kroon. FPT algorithms to compute the elimination distance to bipartite graphs and more. In 47th International Workshop on Graph-Theoretic Concepts in Computer Science, WG 2021, volume 12911 of Lecture Notes in Computer Science, pages 80-93. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86838-3_6.
  27. Bart MP Jansen, Jari JH 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, STOC 2021, pages 1757-1769, 2021. Google Scholar
  28. Ken-ichi Kawarabayashi and Mikkel Thorup. The Minimum k-way Cut of bounded size is fixed-parameter tractable. In Proceedings of the IEEE 52nd Annual Symposium on Foundations of Computer Science, FOCS 2011, pages 160-169. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/FOCS.2011.53.
  29. Wojciech Kazana and Luc Segoufin. Enumeration of monadic second-order queries on trees. ACM Transactions on Computational Logic, 14(4):25:1-25:12, 2013. URL: https://doi.org/10.1145/2528928.
  30. Wojciech Kazana and Luc Segoufin. First-order queries on classes of structures with bounded expansion. Log. Methods Comput. Sci., 16(1), 2020. Google Scholar
  31. Stephan Kreutzer and Siamak Tazari. Lower bounds for the complexity of monadic second-order logic. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pages 189-198. IEEE Computer Society, 2010. Google Scholar
  32. Alexander Lindermayr, Sebastian Siebertz, and Alexandre Vigny. Elimination distance to bounded degree on planar graphs. In Proceedings of the 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, volume 170 of LIPIcs, pages 65:1-65:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  33. Daniel Lokshtanov, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Fixed-parameter tractability of Graph Isomorphism in graphs with an excluded minor, 2021. Manuscript. Google Scholar
  34. Daniel Lokshtanov, M. S. Ramanujan, Saket Saurabh, and Meirav Zehavi. Reducing CMSO model checking to highly connected graphs. In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, volume 107 of LIPIcs, pages 135:1-135:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.135.
  35. Daniel Lokshtanov, Saket Saurabh, and Vaishali Surianarayanan. A parameterized approximation scheme for Min k-Cut. In Proceedings of the 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, pages 798-809. IEEE, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00079.
  36. 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 v1, 2021. URL: http://arxiv.org/abs/2111.03725.
  37. Mihai Pătraşcu and Mikkel Thorup. Planning for fast connectivity updates. In Proceedings of the 48th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2007, pages 263-271. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/FOCS.2007.54.
  38. Saket Saurabh and Meirav Zehavi. Parameterized complexity of multi-node hubs. In Proceedings of the 13th International Symposium on Parameterized and Exact Computation, IPEC 2018, volume 115 of LIPIcs, pages 8:1-8:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.IPEC.2018.8.
  39. Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny. First-order logic with connectivity operators. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2022. Google Scholar
  40. Nicole Schweikardt, Luc Segoufin, and Alexandre Vigny. Enumeration for FO queries over nowhere dense graphs. In Proceedings of the 37th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2018, pages 151-163. ACM, 2018. URL: https://doi.org/10.1145/3196959.3196971.
  41. Szymon Toruńczyk. Aggregate queries on sparse databases. In Proceedings of the 39th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS 2020, pages 427-443. ACM, 2020. Google Scholar
  42. Jan van den Brand and Thatchaphol Saranurak. Sensitive distance and reachability oracles for large batch updates. In 60th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2019, pages 424-435. IEEE Computer Society, 2019. URL: https://doi.org/10.1109/FOCS.2019.00034.
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