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 fixedparameter 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 firstorder logic with atoms for connectivity under vertex failures. We prove that the modelchecking problem for separator logic is fixedparameter 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 firstorder logic within each bag individually. Guided by this observation, we design our modelchecking algorithm using dynamic programming over the tree decomposition, where the transition at each bag amounts to running a suitable modelchecking subprocedure for plain firstorder 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 FirstOrder Logic with Connectivity Under Vertex Failures}},
booktitle = {49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
pages = {102:1102:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772358},
ISSN = {18688969},
year = {2022},
volume = {229},
editor = {Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16443},
URN = {urn:nbn:de:0030drops164432},
doi = {10.4230/LIPIcs.ICALP.2022.102},
annote = {Keywords: Combinatorics and graph theory, Computational applications of logic, Data structures, Fixedparameter algorithms and complexity, Graph algorithms}
}
Keywords: 

Combinatorics and graph theory, Computational applications of logic, Data structures, Fixedparameter 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 