2024/06/26 by Sau, Ignasi, Stamoulis, Giannos, Thilikos, Dimitrios M. · 2 citations
#05C69 #05C75 #05C83 #5C85 #68R10 #Data Structures and Algorithms (cs.DS) #F.2.2 #FOS: Computer and information sciences #G.2.2 #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2406.18465
Given a graph G and a vertex set X, the annotated treewidth tw(G,X) of X in G is the maximum treewidth of an X-rooted minor of G, i.e., a minor H where the model of each vertex of H contains some vertex of X. That way, tw(G,X) can be seen as a measure of the contribution of X to the tree-decomposability of G. We introduce the logic CMSO/tw as the fragment of monadic second-order logic on graphs obtained by restricting set quantification to sets of bounded annotated treewidth. We prove the following Algorithmic Meta-Theorem (AMT): for every non-trivial minor-closed graph class, model checking for CMSO/tw formulas can be done in quadratic time. Our proof works for the more general CMSO/tw+dp logic, that is CMSO/tw enhanced by disjoint-path predicates. Our AMT can be seen as an extension of Courcelle's theorem to minor-closed graph classes where the bounded-treewidth condition in the input graph is replaced by the bounded-treewidth quantification in the formulas. Our results yield, as special cases, all known AMTs whose combinatorial restriction is non-trivial minor-closedness.