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
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.
- Courcelle, Bruno (1990), "The monadic second-order logic of graphs. I. Recognizable sets of finite graphs", Information and Computation 85 (1): 12–75, doi:10.1016/0890-5401(90)90043-H, MR 1042649
- Kneis, Joachim; Langer, Alexander (2009), "A practical approach to Courcelle's theorem", Electronic Notes in Theoretical Computer Science 251: 65–81, doi:10.1016/j.entcs.2009.08.028.
- Lampis, Michael (2010), "Algorithmic meta-theorems for restrictions of treewidth", in de Berg, Mark; Meyer, Ulrich, Proc. 18th Annual European Symposium on Algorithms, Lecture Notes in Computer Science 6346, Springer, pp. 549–560, doi:10.1007/978-3-642-15775-2_47.