[1][2][3] The result was first proved by Bruno Courcelle in 1990[4] and independently rediscovered by Borie, Parker & Tovey (1992).
(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 MSO1 property
[11] Another direction for extending Courcelle's theorem concerns logical formulas that include predicates for counting the size of the test.
which tests whether the cardinality of set S is congruent to r modulo q. Courcelle's theorem can be extended to these logics.
[4] As stated above, Courcelle's theorem applies primarily to decision problems: does a graph have a property or not.
However, the same methods also allow the solution to optimization problems in which the vertices or edges of a graph have integer weights, and one seeks the minimum or maximum weight vertex set that satisfies a given property, expressed in second-order logic.
These optimization problems can be solved in linear time on graphs of bounded clique-width.
[8][11] Rather than bounding the time complexity of an algorithm that recognizes an MSO property on bounded-treewidth graphs, it is also possible to analyze the space complexity of such an algorithm; that is, the amount of memory needed above and beyond the size of the input itself (which is assumed to be represented in a read-only way so that its space requirements cannot be put to other purposes).
[6] In more detail, two graphs G1 and G2, each with a specified subset T of vertices called terminals, may be defined to be equivalent with respect to an MSO formula F if, for all other graphs H whose intersection with G1 and G2 consists only of vertices in T, the two graphs G1 ∪ H and G2 ∪ H behave the same with respect to F: either they both model F or they both do not model F. This is an equivalence relation, and it can be shown by induction on the length of F that (when the sizes of T and F are both bounded) it has finitely many equivalence classes.
Therefore, it is possible to perform a bottom-up computation on this tree decomposition, computing an identifier for the equivalence class of the subtree rooted at each bag by combining the edges represented within the bag with the two identifiers for the equivalence classes of its two children.
This non-elementary complexity is necessary, in the sense that (unless P = NP) it is not possible to test MSO properties on trees in a time that is fixed-parameter tractable with an elementary dependence on the parameter.
[16] The proofs of Courcelle's theorem show a stronger result: not only can every (counting) monadic second-order property be recognized in linear time for graphs of bounded treewidth, but also it can be recognized by a finite-state tree automaton.
Courcelle conjectured a converse to this: if a property of graphs of bounded treewidth is recognized by a tree automaton, then it can be defined in counting monadic second-order logic.
The general version of the conjecture was finally proved by Mikołaj Bojańczyk and Michał Pilipczuk.
The same is true more generally for certain classes of graphs in which a tree decomposition can itself be described in MSOL.
The proof is based on a theorem of Robertson and Seymour that the families of graphs with unbounded treewidth have arbitrarily large grid minors.
[23] Grohe (2001) used Courcelle's theorem to show that computing the crossing number of a graph G is fixed-parameter tractable with a quadratic dependence on the size of G, improving a cubic-time algorithm based on the Robertson–Seymour theorem.
If the given graph G has small treewidth, Courcelle's theorem can be applied directly to this problem.
Grohe's algorithm performs these simplifications until the remaining graph has a small treewidth, and then applies Courcelle's theorem to solve the reduced subproblem.
[24][25] Gottlob & Lee (2007) observed that Courcelle's theorem applies to several problems of finding minimum multi-way cuts in a graph, when the structure formed by the graph and the set of cut pairs has bounded treewidth.
[26] In computational topology, Burton & Downey (2014) extend Courcelle's theorem from MSO2 to a form of monadic second-order logic on simplicial complexes of bounded dimension that allows quantification over simplices of any fixed dimension.
As a consequence, they show how to compute certain quantum invariants of 3-manifolds as well as how to solve certain problems in discrete Morse theory efficiently, when the manifold has a triangulation (avoiding degenerate simplices) whose dual graph has small treewidth.