Co-Decompositions and FO Model Checking

Abstract

Tree decompositions describe large graphs as gluings of smaller component parts. Here we study their categorical duals, tree co-decompositions, which construct large graphs via fibered products of small constituent parts. Co-decompositions are compressed representations of graphs or relational structures: the decomposed object can be exponentially larger than the space required to specify the co-decomposition. Our main contribution is an algorithmic meta-theorem for first order logic: given only a co-decomposition of a $\sigma$-structure $G$ with $b$ bags, each of size at most $w$ and an FO sentence $\varphi$, there is an algorithm which, without ever constructing or inspecting $G$, operates on the co-decomposition and determines whether $G\models \varphi$ in time $f_{\sigma }(w,|\phi |)\cdot b$. We pair this algorithm with structural results on tree co-width, including its relationship to tree-width and a separation from twin-width. Furthermore, we characterize bounded path co-width using a graph grammar. In contrast to our logical meta-theorem, we prove that $(s,t)$-Path becomes NP-hard on co-decomposition inputs. These results demonstrate how categorical constructions can enable efficient computation on exponentially compressed structures.

arXiv comment63 pages, 12 figures