Fixed-Point Definability and Polynomial Time on Graphs with Excluded Minors

We prove that fixed-point logic with counting captures polynomial time on all classes of graphs with excluded minors. That is, for every class C of graphs such that some graph H is not a minor of any graph in C, a property P of graphs in C is decidable in polynomial time if and only if it is definable in fixed-point logic with counting. Furthermore, we prove that for every class C of graphs with excluded minors there is a k such that the k-dimensional Weisfeiler-Lehman algorithm decides isomorphism of graphs in C in polynomial time. The Weisfeiler-Lehman algorithm is a combinatorial algorithm for testing isomorphism. It generalises the basic colour refinement algorithm and is much simpler than the known group-theoretic algorithms for deciding isomorphism of graphs with excluded minors. The main technical theorem behind these two results is a "definable structure theorem" for classes of graphs with excluded minors. It states that graphs with excluded minors can be decomposed i...

• Type: Journal
• Year: 2010
• Where: LICS
• Authors: Martin Grohe
• Keywords: Algorithms, Automated Reasoning, Fixed-point Logic, LICS 2010, Polynomial Time