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 \((\mathsf{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^{\mathcal{O}(\mathsf{td})} n^{\mathcal{O}(1)}\) and space \(n^{\mathcal{O}(1)}\) on \(n\)-vertex graphs provided with elimination forests of depth \(\mathsf{td}\). We provide a model checking algorithm for \(\mathsf{NEO_2[FRec]\!+\!ACK}\) with such complexity that unifies and extends these results. For \(\mathsf{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 \(\mathcal{O}(\mathsf{td}\log (n))\).