Courcelle's theorem

In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in monadic second-order logic can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bruno Courcelle in 1990 and is considered the archetype of algorithmic meta-theorems.

In this context, the graph is described by a set of vertices V and a binary adjacency relation, and the restriction to monadic logic means that the graph property in question may be defined in terms of sets of vertices of the given graph, but not in terms of sets of edges. As an example, the property of a graph being colorable with three colors (represented by three sets of vertices R, G, and B) may be defined by the monadic second-order formula

$\begin{align}\exists R,G,B \,&\bigl(\forall v\in V (v\in R\vee v\in G\vee v\in B)\bigr)\wedge\\& \bigl(\forall u,v \,((u\in R\wedge v\in R)\vee (u\in G\wedge v\in G)\vee (u\in B\wedge v\in B))\to\lnot\mathrm{adj}(u,v)\bigr).\end{align}$

The first part of this formula ensures that the three color classes cover all the vertices of the graph, and the second ensures that they each form an independent set. Thus, by Courcelle's theorem, 3-colorability of graphs of bounded treewidth may be tested in linear time.

The typical approach to proving Courcelle's theorem involves the construction of a finite bottom-up tree automaton that performs a tree decomposition of the graph to recognize it.