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.

翻译：对于图$G$，参数树深度度量所有森林$F$（称为消去森林）的最小深度，其中$G$是$F$的祖先-后代闭包的子图。我们引入一种称为带无环性、连通性和团约束的邻域算子逻辑（简记为$\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$），该逻辑能刻画所有已知在具有深度$k$的消去森林的$n$顶点图上可在$2^{\mathcal{O}(k)}n^{\mathcal{O}(1)}$时间和$n^{\mathcal{O}(1)}$空间内求解的NP难问题——如独立集或哈密顿回路。我们为$\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$提供了一个具有此类复杂度的模型检测算法，该算法统一并扩展了这些结果。对于$\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{k}$（即上述逻辑中不使用无环性和连通性约束的片段），我们得到了该结果的强化版本，其空间复杂度降低至$\mathcal{O}(k\log(n))$。与[Bergougnoux, Dreier and Jaffke, SODA 2023]中引入的距离邻域逻辑类似，逻辑$\mathsf{NEO}_2[\mathsf{FRec}]+\mathsf{ACK}$是全存在性$\mathsf{MSO}_2$的扩展，增加了以下谓词：(1) 查询顶点集邻域泛化形式的能力，(2) 验证顶点集与边集的连通性与无环性，(3) 验证顶点集是否诱导出一个团。我们的结果为某些问题提供了$2^{\mathcal{O}(k)}n^{\mathcal{O}(1)}$时间和$n^{\mathcal{O}(1)}$空间的算法，而这类算法此前是否存在是未知的。特别地，$\mathsf{NEO}_2[\mathsf{FRec}]$通过CNF公式对应的关联图刻画了CNF-SAT问题，同时也能刻画若干模计数问题，如奇支配集问题。