Our new paper, Co-Decompositions and FO Model Checking, is finally on the arXiv! This is joint work with Will Turner, Laura Larios-Jones and Guilherme Gomes, and I’m really happy to see it out in the world.
The project started with some research I was doing with Will Turner, and then developed through various visits here at USP: Will and Laura did research internships with me at USP, and Guilherme hopped on over from Minas Gerais to spend a week with us in person too. One of the nicest parts of my job is getting to do mathematics with wonderful people, and this project has been a particularly enjoyable example of that.
So, what’s a co-decomposition of graphs? Well, the category-theoretic definition is simple: it is a structured decomposition values in \(\mathbf{Grph}^{\mathrm{op}}\). Take a tree \(T\), consider its category of elements \(\int T\), and take a diagram
\[
\mathcal d \colon \int T \to \mathbf{Grph}^{\mathrm{op}}
\]
whose morphisms are monomorphisms. That’s it! The resulting graph is the colimit of this diagram in \(\mathbf{Grph}^{\mathrm{op}}\). Equivalently, removing a layer of duality: a tree co-decomposition is a special kind of diagram of epimorphisms of graphs and we are interested in studying its limit in \(\mathbf{Grph}\). Said a third way for good measure: a co-decomposition is essentially a tree decomposition with all the arrows reversed.
Of course, this is not quite how we present things in the paper. We wanted our work to be accessible to combinatorialists, so we give a more concrete definition: take a tree \(T\), put a graph \(G_t\) at each node \(t\) (a bag) and a graph \(G_e\) at each edge \(e\) (an adhesion), and equip every incidence \(t\in e\) with an epimorphism \(G_t\twoheadrightarrow G_e\). The graph we’re interested in is then obtained by taking successive pullbacks of these pieces. This is the dual picture to the usual tree decomposition, where we glue smaller graphs together along common subgraphs.
What makes these co-decompositions interesting is that they can be extremely compressed representations of graphs. A co-decomposition with \(b\) bags of size at most \(w\) can describe a graph with as many as \(w^b\) vertices! This leads to a rather natural algorithmic question: can we solve problems on the enormous graph without ever actually constructing it?
The main result of our paper says that, for properties expressible in first-order logic, the answer is yes! We prove an algorithmic meta-theorem showing that first-order model checking is fixed-parameter tractable when parameterized by the width of the co-decomposition and the length of the formula. Better still, the algorithm runs in linear time in the number of bags (with a rather large parameter-dependent constant). We also prove various structural results about co-width and, rather surprisingly, show that even finding a path between two specified vertices becomes NP-hard when the graph is given by a co-decomposition (note that \((s,t)\)-Path is not FO-expressable).
There is something else about this result that I find particularly interesting. In much of my previous work, I’ve used category theory to generalize algorithmic results: Id take something I already understood for graphs and I’d extend it to much more general mathematical structures. In contrast, this is the first time I’ve proved an algorithmic result which, even when restricted to ordinary graphs, I genuinely have no idea how to prove without category theory! Perhaps this says more about my own limitations than it does about the power of category theory, but either way, I find it satisfying.
Anyway, if you’d like to hear more about all of this, I’ll be giving a talk about the paper this Monday, November 9th, at 12:30 (São Paulo time).
Abraços,
Ben