License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2022.102
URN: urn:nbn:de:0030-drops-164432
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16443/
Pilipczuk, Michał ;
Schirrmacher, Nicole ;
Siebertz, Sebastian ;
Toruńczyk, Szymon ;
Vigny, Alexandre
Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures
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.
BibTeX - Entry
@InProceedings{pilipczuk_et_al:LIPIcs.ICALP.2022.102,
author = {Pilipczuk, Micha{\l} and Schirrmacher, Nicole and Siebertz, Sebastian and Toru\'{n}czyk, Szymon and Vigny, Alexandre},
title = {{Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures}},
booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
pages = {102:1--102:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-235-8},
ISSN = {1868-8969},
year = {2022},
volume = {229},
editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16443},
URN = {urn:nbn:de:0030-drops-164432},
doi = {10.4230/LIPIcs.ICALP.2022.102},
annote = {Keywords: Combinatorics and graph theory, Computational applications of logic, Data structures, Fixed-parameter algorithms and complexity, Graph algorithms}
}
|
Keywords: |
|
Combinatorics and graph theory, Computational applications of logic, Data structures, Fixed-parameter algorithms and complexity, Graph algorithms |
|
Collection: |
|
49th International Colloquium on Automata, Languages, and Programming (ICALP 2022) |
|
Issue Date: |
|
2022 |
|
Date of publication: |
|
28.06.2022 |
