Courcelle's theorem

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

In one variation of monadic second-order graph logic known as MSO₁, the graph is described by a set of vertices V and a binary adjacency relation adj(.,.), 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 or of tuples of vertices.

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

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. (It would also be possible to add clauses to the formula to ensure that the three color classes are disjoint, but this makes no difference to the result.) Thus, by Courcelle's theorem, 3-colorability of graphs of bounded treewidth may be tested in linear time.

For this variation of graph logic, Courcelle's theorem can be extended from treewidth to clique-width: for every fixed MSO₁ property P, and every fixed bound b on the clique-width of a graph, there is a linear-time algorithm for testing whether a graph of clique-width at most b has property P. The original formulation of this result required the input graph to be given together with a construction proving that it has bounded clique-width, but later approximation algorithms for clique-width removed this requirement.

...
Wikipedia