vix.ing · top · new · best · stats · spec

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

2025/10/22 by Benjamin Bergougnoux, Bergougnoux, Benjamin, Vera Chekan +3
Computer Science · #05C85 #68Q27 #Advanced Graph Theory Research #Complexity and Algorithms in Graphs #Computational complexity theory #Constraint Satisfaction and Optimization #Data Structures and Algorithms (cs.DS) #Dominating set #Exponential function #Extension (predicate logic) #F.2.2 #FOS: Computer and information sciences #Graph #Logic in Computer Science (cs.LO) #Modulo #Time complexity #Vertex (graph theory) #Vertex cover

paper · pdf · doi:10.48550/arxiv.2510.19793

openalex publication_date 2025/10/22 · openalex created_date 2025/10/24 · openalex updated_date 2026/08/04

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

Related