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

TL;DR

This work introduces neighborhood operator logic with acyclicity, connectivity, and clique constraints, NEO_2[FRec]+ACK, to capture NP-hard problems that are solvable in 2^{O(td)} n^{O(1)} time and polynomial space when given an elimination forest of depth td. It extends fully-existential MSO_2 with neighborhood operators and modular counting via finitely recognizable sets, enabling a model-checking algorithm that unifies and extends known results, and, in the NEO_2[FRec]+K fragment, achieves O(td log n) space. The approach relies on representing partial solutions as polynomials and combining them with discrete Fourier transforms on the elimination-tree structure, using inclusion-exclusion to enforce constraints like acyclicity and connectivity, and Cut&Count for randomized handling of connectivity. The results yield 2^{O(td)} time and polynomial or low-degree logarithmic space algorithms for a broad family of problems (including CNF-SAT on incidence graphs and modulo-counting problems), advancing the frontier of logic-based meta-theorems for treedepth-based fixed-parameter tractability. The framework suggests several directions for derandomization, improved space bounds, and extending the methodology to further problems via even richer variants of neighborhood predicates.

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.

Figures (2)

• Figure 1: Illustration of an elimination tree of a graph with two distinguished leaves $w$ and $w'$; the edges of the tree are depicted in light grey. The vertices $b$ with $\mathsf{left}(b)=w$ are depicted in blue. The (thick) blue edges are the edges of $\mathsf{sheaf}(w)$ and the (thick) magenta edges are the edges of $\mathsf{sheaf}(w_2)$.
• Figure 2: Illustration of the transformation from a graph $G$ to the graph $\vec{G}_\varphi$. The edge $uv\in E(G)$ on the left corresponds to the arcs $(u^1,v^1),\ldots,(u^1,v^{d_\varphi})$ and $(v^1,u^1),\ldots,(v^1,u^{d_\varphi})$ on the right.

Theorems & Definitions (91)

• Definition 1.1
• Definition 1.2
• Theorem 1.3
• Theorem 1.4
• Theorem 3.3
• Theorem 3.4
• Theorem 3.5: cygan2015parameterized, Theorem 10.2
• Definition 4.1
• Lemma 4.2
• proof