Courcelle's Theorem and Monadic Second Order Logic (MSO)

Now there are all kinds of so-called “meta-theorems” that connect logic and graph algorithms. Here’s a pretty cool one using a logic you may not have heard of: the monadic second-order logic of graphs. You see, Courcelle’s theorem says that for graphs of bounded treewidth, properties definable in this “MSO” logic can be decided in linear time. This makes the graph problem fixed parameter tractable parameterized by treewidth. The proof involves some fairly heavy machinery (or at least terminology I’m not super familiar with) so I personally find the primary literature quite hard to follow and you do have to be a little bit careful what the exact conditions are if you’re going to use it for real, but you know the drill: look it up. Here’s a sketch though.

In this monadic second order logic of graphs, you’re allowed existential and universal quantification over vertices, edges, sets of vertices, and sets of edges; then you have a set membership predicate and an adjacency predicate for the graph. For example, three-colouring goes like this:

$\exists R, G, B \subseteq V\colon$

$\phantom{\land\ } (\forall v\in V\colon ( v \in R \lor v \in G \lor v \in B ))$

$\land\ (\forall u,v\in V\colon u\in R\land v\in R\implies \neg\text{adj}(u,v))$

$\land\ (\forall u,v\in V\colon u\in G\land v\in G\implies \neg\text{adj}(u,v))$

$\land\ (\forall u,v\in V\colon u\in B\land v\in B\implies \neg\text{adj}(u,v))$

Now Courcelle says that graphs where this is true – graphs where this formula has a model, if you will – can be recognized in fixed parameter linear time parameterized by the treewidth of the graph.

The size of the formula (the “sentence” in their terminology) also goes into the runtime, in quite a terrible way, but you would typically use Courcelle’s theorem with a fixed formula like the three-colouring one: you’re showing that a particular graph property can be decided in FPT time. This wouldn’t work for general colouring, because the formula gets larger with $n$, but it does work for any particular $k$-colouring. There are also variants that use clique-width instead of treewidth, but you can look that up on your own as well.