A Logic-based Algorithmic Meta-Theorem for Treedepth: Single Exponential FPT Time and Polynomial Space

Vera Chekan ( Humboldt University Berlin )

For a graph G, the parameter treedepth measures the minimum depth among all forests F, called elimination forests, such that G is a subgraph of the ancestor-descendant closure of F. We introduce a logic, called neighborhood operator logic with acyclicity, connectivity and clique constraints (NEO2[FRec]+ACK for short), that captures all NP-hard problems—like Indepen- dent Set or Hamiltonian Cycle—that are known to be tractable in time 2^O(td) n^O(1) and space n^O(1) on n-vertex graphs provided with elimination forests of depth td. We provide a model checking algorithm for NEO2[FRec]+ACK with such complexity that unifies and extends these results. For NEO2[FRec]+K, the fragment of the above logic that does not use acyclicity and connectivity constraints, we get a strengthening of this result, where the space complexity is reduced to O(td log(n)). With a similar mechanism as the distance neighborhood logic introduced in [Bergoug- noux, Dreier and Jaffke, SODA 2023], the logic NEO2[FRec]+ACK is an extension of the fully- existential MSO2 with predicates for (1) querying generalizations of the neighborhoods of vertex sets, (2) verifying the connectivity and acyclicity of vertex and edge sets, and (3) verifying that a vertex set induces a clique. Interestingly, NEO2[FRec], the fragment of NEO2[FRec]+K that does not use clique constraints, is equivalent (up to minor features) to a variant of modal logic— introduced in [Pilipczuk, MFCS 2011]—that captures many problems known to be tractable in single exponential time when parameterized by treewidth. Our results provide 2^O(td) n^O(1) time and n^O(1) space algorithms for problems for which the existence of such algorithms was previously unknown. In particular, NEO2[FRec] captures CNF-SAT via the incidence graphs associated to CNF formulas, and it also captures several modulo counting problems like Odd Dominating Set. To prove our results, we extend the applicability of algebraic transforms such as the inclusion- exclusion principle and the discrete Fourier transform. To our knowledge, this is the first time, the discrete Fourier transform have been used to obtain space-efficient algorithms on graphs of bounded treedepth. To achieve the logspace complexity for NEO2[FRec]+K, we also use the technique from [Pilipczuk and Wrochna, ACM Trans. Comput. Theory 2018] based on Chinese remainder theorem. This is a joint work with Benjamin Bergougnoux and Giannos Stamoulis.