Monadic second order logic and treewidth

Ron Fagin is a great theorist who has made many important contributions to diverse aspects of computing. He is perhaps most famous for his brilliant categorization of polynomial time by second order logic—Fagin’s Theorem.

Today I plan on talking about a related theorem—Courcelle’s—proved in 1990. Yet the theorem is not, in my opinion, as well known as it should be. The truth is I did not know this pretty theorem until I ran across it the other day. So perhaps everyone else knows Courcelle’s result except for me. Oh well.

Courcelle’s Theorem

Bruno Courcelle’s theorem is quite striking, in my opinion:

Theorem: Let ${\phi}$ be any graph property that is definable in MSO logic. For any fixed ${k}$, the there is a linear time algorithm for testing the property ${\phi}$ on any graph of treewidth at most ${k}$.

I will explain the theorem and try to give a high level view of its proof. But, even if the concepts of MSO—Monadic Second Order—logic and treewidth are new to you, the theorem should still be striking. There are a few theorems of the form: any graph property expressible in a powerful logic is computable on a class of graphs in linear time.

Treewidth

The concept of treewidth is fairly widely known, and was used extensively in the famous work of Neil Robertson and Paul Seymour on graph minors. I will include a definition here for completeness. My intuition is that for most graph problems the case of trees is easy: for example, there is a linear time algorithm for tree isomorphism. The notion of small tree width is an attempt—a very successful attempt—to generalize trees to include a much larger class of graphs.

A tree decomposition of a graph ${G = (V,E)}$ is a composed of a family of sets of vertices, called bags, ${B_{1},\dots,B_{m}}$ and a tree ${T}$ on the nodes ${1,\dots,m}$ with these properties:

• Every vertex of ${G}$ is in at least one bag.
• Every edge of ${G}$ has both endpoints in some bag.
• For all vertices of ${G}$, the set of bags that contain the vertex form a subtree of ${T}$.

The last is more precisely: for all vertices ${v}$ of ${G}$ the set ${\{i \mid v \in B_{i} \}}$ is a subtree of ${T}$. The width of the decomposition is the maximum of ${|B_{i}|-1}$ over all ${i}$. The treewidth of a graph ${G}$, ${\mathbf{tw}(G)}$ is the minimum such width over all valid tree decompositions. The ${-1}$ is there to make the treewidth of a tree ${1}.$

Here is an example, from our friends at Wikipedia, of a graph and a decomposition:

MSO

Suppose that ${E(x,y)}$ stands for the edge relationship of some simple undirected graph. Then, first order sentences allow variables only over vertices. For example, the sentence

$\displaystyle \forall x,y,z \ E(x,y) \wedge E(y,z) \rightarrow \neg E(y,x)$

means that the graph has no triangle. This is a first order sentence, since all the variables range over vertices of the graph.

First order sentences can capture some interesting properties—they can express the property of having a ${k}$-clique for any fixed ${k}$. However, first order is too weak to expressive many important graph properties such as the property: a graph is ${k}$-colorable.

This leads to the idea to extend the first order logic to allow more powerful variables. A natural notion is to allow variables to range over arbitrary sets of tuples of vertices: this is called Second Order (SO) logic. This theory is very powerful, since Fagin’s Theorem is:

Theorem: Properties expressible by second-order logic existential sentences are precisely the complexity class NP.

An existential sentence is a sentence of the form:

$\displaystyle \exists R \exists S \dots \phi(R,S)$

where ${R}$ and ${S}$ and ${\dots}$ range over relations and ${\phi}$ is a first order formula.

Clearly, there are properties of this form requiring more than linear time—even on trees. This is the reason that Courcelle’s Theorem must restrict the properties to Monadic Second Order (MSO) logic. A sentence is a monadic one provided all the second order variables range over sets. Notice that being expressible in MSO logic is a stronger requirement than being expressible in Second Order logic: MSO is a subset of Second Order logic.

It is now easy to define ${k}$-colorable. Here is how to express ${3}$-colorable:

$\displaystyle \exists A \exists B \exists C \ \phi(A,B,C)$

where ${\phi(A,B,C)}$ uses first order quantifiers to check ${A,B,C}$ form a partition of the vertices, and that if ${E(x,y)}$ then ${x}$ and ${y}$ are colored differently. Think of ${A(x)}$ as meaning ${x}$ is colored “A,” and the same for the other sets.

The logic MSO is quite powerful, but is still not powerful enough to define some properties: for example, the property of having a Hamiltonian Circuit, is not definable in MSO.

Proof Idea

The proof of Courcelle’s theorem is based on two key ideas:

1. The ability to find a ${k}$-treewidth decomposition in linear time.
2. The ability to check the MSO property on a tree decomposition in linear time.

The first is a result due to Hans Bodlaender, who improved the original algorithm of Robertson and Seymour from quadratic time; see this for a nice survey and discussion of algorithms for finding treewidth.

Once a tree decomposition is found the key is a tree automaton can be constructed to check the MSO sentence. Tree automata are a generalization of finite automata from linear words to finite trees. Luckily many of the same constructions and properties of finite automata carry over to tree automata, this allows the checking to be done in linear time.

Open Problems

The Courcelle theorem is, in my opinion, quite pretty. However, the hidden constants are huge, and an obvious question is when can “real” linear time algorithms be found for properties expressible in MSO? Another interesting open problem is what is the largest class of sentences of SO that lead to linear time algorithms on graphs of bounded treewidth?

March 9, 2010 12:21 am

I agree with you: the theorem is definitely not known enough. Would you happen to know a good place that shows how to phrase many many standard graph problems in MSO logic? Students always keep asking me for more examples…

There are some ways to extend MSO logic so that it covers more graph problems but is still polynomial on partial k-trees. The paper by Gupta et al. from SWAT 96 is a decent overview.

• March 12, 2010 7:45 am

Bruno Courcelle mentioned last year that some of the people on his team were working on a collection of optimised MSO fragments that could be used as building blocks. If I understood him correctly, in some cases it is possible to produce small tree automata by careful hand coding, avoiding the huge blowup in the standard translation (pointed out by Moshe Vardi below).

Leonid Libkin’s book “Elements of Finite Model Theory” has a small but well-described set of fragments expressing various properties, mostly graph theoretic.

• March 12, 2010 7:55 am

Modal and temporal logic are fragments of MSO that allow an exponential translation to automata.

2. March 9, 2010 12:35 am

There are two separate constants here. The first is the constant in the linear-time algorithm for finding tree decompositions. One could hope for an improved algorithm here. The second constant comes from the translation of MSO formulas to tree automata, which is non-elementary, i.e., the blow-up cannot be bounded by a fixed tower of exponential. See M. Frick and M. Grohe. The complexity of first-order and monadic second-order logic revisited. In LICS’02, pages 215–224, 2002.

March 10, 2010 5:00 am

With respect to your second question: “what is the largest fragment of SO that gives linear-time algorithms on graphs of bounded tree-width?” Courcelle’s Theorem applies to a stronger version of MSO, sometimes called MSO2 and considered by Courcelle himself, where in addition to quantifiers that range over sets you can also use quantifiers that range over subsets of edges. The reason this works is that if a graph has bounded treewidth then its incidence bipartite graph also has bounded treewidth. This new logic is more expressive: for example it can express Hamiltonicity which is the example you gave of an NP-property not definable in MSO.

4. March 11, 2010 5:56 pm

I think there is an error in the “no-triangle” graph example of FO. Did you mean to write:

not E(z,x)

in the end?

March 11, 2010 7:32 pm

Yes. Thanks for this.

5. March 13, 2010 5:21 am

Dear Richard, thanks for your note on « my theorem », and also to those who made comments.
This result is presented in the books on fixed parameter tractability by Downey and Fellows (1999) and Flum and Grohe (2006).
There are actually two theorems:
* the one you present, for bounded tree-width and MSO properties on incidence graphs (they can use edge set quantifications and express Hamiltonicity and perfect matching), and
* one for bounded clique-width and MSO properties (without edge set quantifications; Courcelle, Makowsky, Rotics, Discrete Applied Maths 2001).

Clique-width is a graph complexity measure similar to tree-width but more powerful : cliques have clique-width 2 and unbounded tree-width, and bounded tree-width implies bounded clique-width. The corresponding parsing problem, considered by Oum, Seymour and Hlineny is more difficult than for tree-width. Yet, there are “only” cubic approximation algorithms: they give fixed-parameter cubic algorithms.

For obtaining usable algorithms, I. Durand (LaBRI, Bordeaux) and myself propose :
* not to “compile” tree-automata, but to recompute their transitions whenever needed,
* to apply this to MSO sentences written without negation but instead, with basic graph properties for which deterministic automata are defined “combinatorially” and not compiled.

This idea is presented in an accepted communication to the European LISP Symposium in Portugal, May 2010. See: http://www.labri.fr/perso/courcell/ArticlesEnCours/BCDurandLISP.pdf

Detailed proofs are in a book in preparation: see Chapter 6 of :
http://www.labri.fr/perso/courcell/Book/CourGGBook.pdf

Makowsky and Marino (Tree-width and the Monadic Quantifier Hierarchy, Theor. Comput. Sci. 303 (2003) 157-170) have proved that if every existential monadic second-order property (3-vertex colorability is of this form) is decidable in polynomial time on all graphs of a set C that is closed under taking minors or topological minors, then C has bounded tree-width. S. Kreutzer has results of this type.

March 13, 2010 11:45 am

Thanks for the information. Your results should be widely known, and I hope in some small way I have helped.

March 23, 2010 6:20 pm

Hello Richard,
as was already pointed out, the theorem you are writing about is capable of expressing Hamiltonicity (as we just did today at school 😉 ) . It is easy to write a formula that is satisfied when a graph has a 2-factor (a cycle decomposition), the “tricky” part is to express that it is connected. The way to do it is to say that there doesn’t exist a partition of vertices into two disjoint sets V1, V2 such that there is no edge between them. (This is my first time commenting here so excuse me for not being able to use the mathematical expressions capabilities of your blog).
al-Quaknaa

• March 24, 2010 6:07 am

al-Quaknaa: as you point out, graph connectivity is the heart of the issue. However, the negation of an $exists$MSO sentence is only $exists$MSO in very special cases, and this is not one of them.

March 24, 2010 8:41 am

András Salamon: I’m not sure what you mean. This formula is taken from my professor’s lecture notes:

could you please tell me what is wrong with it? Thank you.