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 one variation of monadic second-order graph logic known as MSO1, 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
∃R,G,B. (∀v∈V. (v∈R ∨ v∈G ∨ v∈B)) ∧ (∀u,v∈V. ((u∈R ∧ v∈R) ∨ (u∈G ∧ v∈G) ∨ (u∈B ∧ v∈B)) → ¬adj(u,v)).
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 MSO1 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.
Courcelle's theorem may also be used with a stronger variation of monadic second-order logic known as MSO2. In this formulation, a graph is represented by a set V of vertices, a set E of edges, and an incidence relation between vertices and edges. This variation allows quantification over sets of vertices or edges, but not over more complex relations on tuples of vertices or edges.
For instance, the property of having a Hamiltonian cycle may be expressed in MSO2 by describing the cycle as a set of edges that includes exactly two edges incident to each vertex, such that every nonempty proper subset of vertices has an edge in the cycle with exactly one endpoint in the subset. However, Hamiltonicity cannot be expressed in MSO1.
Another direction for extending Courcelle's theorem concerns logical formulas that include predicates for counting the size of the test. In this context, it is not possible to perform arbitrary arithmetic operations on set sizes, nor even to test whether two sets have the same size. However, MSO1 and MSO2 can be extended to logics called CMSO1 and CMSO2, that include for every two constants q and r a predicate which tests whether the cardinality of set S is congruent to r modulo q. Courcelle's theorem can be extended to these logics.
Satisfiability and Seese's theorem
The satisfiability problem for a formula of monadic second-order logic is the problem of determining whether there exists at least one graph (possibly within a restricted family of graphs) for which the formula is true. For arbitrary graph families, and arbitrary formulas, this problem is undecidable. However, satisfiability of MSO2 formulas is decidable for the graphs of bounded treewidth, and satisfiability of MSO1 formulas is decidable for graphs of bounded clique-width. The proof involves building a tree automaton for the formula and then testing whether the automaton has an accepting path.
As a partial converse, Seese (1991) proved that, whenever a family of graphs has a decidable MSO2 satisfiability problem, the family must have bounded treewidth. The proof is based on a theorem of Robertson and Seymour that the families of graphs with unbounded treewidth have arbitrarily large grid minors. Seese also conjectured that every family of graphs with a decidable MSO1 satisfiability problem must have bounded clique-width; this has not been proven, but a weakening of the conjecture that replaces MSO1 by CMSO1 is true.
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. An additional later improvement to linear time by Kawarabayashi & Reed (2007) follows the same approach. If the given graph G has small treewidth, Courcelle's theorem can be applied directly to this problem. On the other hand, if G has large treewidth, then it contains a large grid minor, within which the graph can be simplified while leaving the crossing number unchanged. 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.
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. As a result they obtain a fixed-parameter tractable algorithm for these problems, parameterized by a single parameter, treewidth, improving previous solutions that had combined multiple parameters.
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.
- Eger, Steffen (2008), Regular Languages, Tree Width, and Courcelle's Theorem: An Introduction, VDM Publishing, ISBN 9783639076332.
- Courcelle, Bruno; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, Encyclopedia of Mathematics and its Applications 138, Cambridge University Press, ISBN 9781139644006, Zbl 1257.68006.
- 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, Zbl 0722.03008
- 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, Zbl 1287.68078.
- Courcelle, B.; Makowsky, J. A.; Rotics, U. (2000), "Linear time solvable optimization problems on graphs of bounded clique-width", Theory of Computing Systems 33 (2): 125–150, doi:10.1007/s002249910009, MR 1739644, Zbl 1009.68102.
- Courcelle & Engelfriet (2012), Proposition 5.13, p. 338.
- Seese, D. (1991), "The structure of the models of decidable monadic theories of graphs", Annals of Pure and Applied Logic 53 (2): 169–195, doi:10.1016/0168-0072(91)90054-P, MR 1114848.
- Courcelle, Bruno; Oum, Sang-il (2007), "Vertex-minors, monadic second-order logic, and a conjecture by Seese", Journal of Combinatorial Theory, Series B 97 (1): 91–126, doi:10.1016/j.jctb.2006.04.003, MR 2278126.
- Grohe, Martin (2001), "Computing crossing numbers in quadratic time", Proceedings of the Thirty-third Annual ACM Symposium on Theory of Computing (STOC '01), pp. 231–236, doi:10.1145/380752.380805.
- Kawarabayashi, Ken-ichi; Reed, Buce (2007), "Computing crossing number in linear time", Proceedings of the Thirty-ninth Annual ACM Symposium on Theory of Computing (STOC '07), pp. 382–390, doi:10.1145/1250790.1250848.
- Gottlob, Georg; Lee, Stephanie Tien (2007), "A logical approach to multicut problems", Information Processing Letters 103 (4): 136–141, doi:10.1016/j.ipl.2007.03.005, MR 2330167.
- Burton, Benjamin A.; Downey, Rodney G. (2014), Courcelle's theorem for triangulations, arXiv:1403.2926. Short communication, International Congress of Mathematicians, 2014.
- Grohe, Martin; Mariño, Julian (1999), "Definability and descriptive complexity on databases of bounded tree-width", Database Theory — ICDT’99: 7th International Conference Jerusalem, Israel, January 10–12, 1999, Proceedings, Lecture Notes in Computer Science 1540, pp. 70–82, doi:10.1007/3-540-49257-7_6.
- Gottlob, Georg; Pichler, Reinhard; Wei, Fang (January 2010), "Bounded treewidth as a key to tractability of knowledge representation and reasoning", Artificial Intelligence 174 (1): 105–132, doi:10.1016/j.artint.2009.10.003.
- Madhusudan, P.; Parlato, Gennaro (2011), "The Tree Width of Auxiliary Storage", Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11), SIGPLAN Notices, 46 (1), pp. 283–294, doi:10.1145/1926385.1926419
- Obdržálek, Jan (2003), "Fast mu-calculus model checking when tree-width is bounded", Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science 2725, pp. 80–92, doi:10.1007/978-3-540-45069-6_7.