A Class of Graph Properties Computable in Linear Time
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.
Bruno Courcelle’s theorem is quite striking, in my opinion:
Theorem: Let be any graph property that is definable in MSO logic. For any fixed , the there is a linear time algorithm for testing the property on any graph of treewidth at most .
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.
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 is a composed of a family of sets of vertices, called bags, and a tree on the nodes with these properties:
- Every vertex of is in at least one bag.
- Every edge of has both endpoints in some bag.
- For all vertices of , the set of bags that contain the vertex form a subtree of .
The last is more precisely: for all vertices of the set is a subtree of . The width of the decomposition is the maximum of over all . The treewidth of a graph , is the minimum such width over all valid tree decompositions. The is there to make the treewidth of a tree
Here is an example, from our friends at Wikipedia, of a graph and a decomposition:
Suppose that stands for the edge relationship of some simple undirected graph. Then, first order sentences allow variables only over vertices. For example, the sentence
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 -clique for any fixed . However, first order is too weak to expressive many important graph properties such as the property: a graph is -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:
where and and range over relations and 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 -colorable. Here is how to express -colorable:
where uses first order quantifiers to check form a partition of the vertices, and that if then and are colored differently. Think of as meaning 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.
The proof of Courcelle’s theorem is based on two key ideas:
- The ability to find a -treewidth decomposition in linear time.
- 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.
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?