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

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 (NEO 2 [FRec]+ACK for short), that captures all NP-hard problems-like Independent 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 NEO 2 [FRec]+ACK with such complexity that unifies and extends these results. For NEO 2 [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 [Bergougnoux, Dreier and Jaffke, SODA 2023 ], the logic NEO 2 [FRec]+ACK is an extension of the fullyexistential MSO 2 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, NEO 2 [FRec], the fragment of NEO 2 [FRec]+K that does not use clique constraints, is equivalent (up to minor features) to a variant of modal logicintroduced 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, NEO 2 [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 inclusionexclusion 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 NEO 2 [FRec]+K, we also use the technique from [Pilipczuk and Wrochna, ACM Trans. Comput. Theory 2018 ] based on Chinese remainder theorem.