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

TL;DR

This paper introduces a new logic-based framework that enables fixed-parameter tractable algorithms with single exponential time and polynomial space for problems on graphs with bounded treedepth, unifying and extending prior results.

Contribution

The paper develops a logic called $ ext{NEO}_2[ ext{FRec}]+ ext{ACK}$ that captures NP-hard problems on graphs with bounded treedepth and provides efficient model checking algorithms for it.

Findings

Achieves $2^{O(k)}n^{O(1)}$ time algorithms for problems on treedepth-bounded graphs.

Reduces space complexity to $O(k \log n)$ for a fragment of the logic.

Captures problems like CNF-SAT and modulo counting problems within the logic framework.

Abstract

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 ($\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$ for short), that captures all NP-hard problems$\unicode{x2013}$like Independent Set or Hamiltonian Cycle$\unicode{x2013}$that are known to be tractable in time $2^{\mathcal{O}(k)}n^{\mathcal{O}(1)}$ and space $n^{\mathcal{O}(1)}$ on $n$-vertex graphs provided with elimination forests of depth $k$. We provide a model checking algorithm for $\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$ with such complexity that unifies and extends these results. For $\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{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 $\mathcal{O}(k\log(n))$. With a similar mechanism as the distance neighborhood logic introduced in [Bergougnoux, Dreier and Jaffke, SODA 2023], the logic $\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$ is an extension of the fully-existential $\mathsf{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. Our results provide $2^{\mathcal{O}(k)}n^{\mathcal{O}(1)}$ time and $n^{\mathcal{O}(1)}$ space algorithms for problems for which the existence of such algorithms was previously unknown. In particular, $\mathsf{NEO}_2[\mathsf{FRec}]$ captures CNF-SAT via the incidence graphs associated to CNF formulas, and it also captures several modulo counting problems like Odd Dominating Set.