Parameterized Complexity of First-Order Logic.
Stephan Kreutzer, Anuj Dawar · Electronic colloquium on computational complexity · 2009
We show that if C is a class of graphs which is nowhere dense then rst-order model-checking is xed-parameter tractable on C. As all graph classes which exclude a xed minor, or are of bounded local tree-width or locally exclude a minor are nowhere dense, this generalises algorithmic meta-theorems obtained for these classes in the past (see [11, 13, 4]). Conversely, if C is not nowhere dense and in addition is closed under taking sub-graphs and satis es some e ectivity conditions then FO-model checking is not FPT on C unless FPT = AW[∗]. Hence, for classes of graphs closed under sub-graphs, this essentially gives a precise characterisation of classes for which FO model-checking is tractable. However, our result generalises to much more general classes of graphs. In particular we show that every class which can e ciently be coloured over a class with the type representation property allows tractable rstorder model-checking. Such classes include all classes which are nowhere dense and also all classes of bounded clique-width. This result therefore uni es all known meta-theorems for rst-order logic.