Théorème de Courcelle

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 . It is considered the archetype of algorithmic meta-theorems. In one variation of monadic second-order graph logic known as MSO1, the graph is described by a set of vertices 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, or sets of tuples of vertices. As an example, the property of a graph being colorable with three colors (represented by three sets of vertices , , and ) may be defined by the monadic second-order formula with the naming convention that uppercase variables denote sets of vertices and lowercase variables denote individual vertices (so that an explicit declaration of which is which can be omitted from the formula). The first part of this formula ensures that the three color classes cover all the vertices of the graph, and the rest 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 MSO1 property , and every fixed bound on the clique-width of a graph, there is a linear-time algorithm for testing whether a graph of clique-width at most has property . 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.