ECCC-Report TR09-131https://eccc.weizmann.ac.il/report/2009/131Comments and Revisions published for TR09-131en-usTue, 19 Mar 2013 14:53:35 +0200
Revision 2
| Parameterized Complexity of First-Order Logic |
Stephan Kreutzer,
Anuj Dawar
https://eccc.weizmann.ac.il/report/2009/131#revision2We consider the model-checking problem for first-order logic, that is, the problem to decide for a given graph $G$ and first-order formula $\varphi$ whether $G\models \varphi$.
Much work has gone into identifying classes $\mathcal{C}$ of graphs on which this problem becomes fixed-parameter tractable, i.e. can be solved in time $f(|\varphi|)\cdot n^c$ for some constant $c$ and computable function $f : \N \rightarrow \N$.
It is known that if $\mathcal{C}$ has locally bounded expansion, then the problem is indeed fixed-parameter tractable on $\mathcal{C}$.
In this note we show that if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal C$ unless FPT = AW[*].
It is still an open problem whether first-order model-checking is fixed-parameter tractable on classes of graphs which are nowhere dense, leaving a gap between our lower bound and the best currently known upper bounds.Tue, 19 Mar 2013 14:53:35 +0200https://eccc.weizmann.ac.il/report/2009/131#revision2
Revision 1
| Parameterized Complexity of First-Order Logic |
Stephan Kreutzer,
Anuj Dawar
https://eccc.weizmann.ac.il/report/2009/131#revision1We show that if $\mathcal C$ is a class of graphs which is
"nowhere dense" then first-order model-checking is
fixed-parameter tractable on $\mathcal C$. As all graph classes which exclude a fixed 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 \cite{FlumGro01,FrickGro01,DawarGroKre07}).
Conversely, if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal 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 efficiently be coloured "over a class with the type representation property" allows tractable first-order model-checking. Such classes include all classes which are nowhere dense and also all classes of bounded clique-width. This result therefore unifies all known meta-theorems for first-order logic.
Tue, 19 Mar 2013 14:21:35 +0200https://eccc.weizmann.ac.il/report/2009/131#revision1
Paper TR09-131
| Parameterized Complexity of First-Order Logic |
Stephan Kreutzer,
Anuj Dawar
https://eccc.weizmann.ac.il/report/2009/131We show that if $\mathcal C$ is a class of graphs which is
"nowhere dense" then first-order model-checking is
fixed-parameter tractable on $\mathcal C$. As all graph classes which exclude a fixed 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 \cite{FlumGro01,FrickGro01,DawarGroKre07}).
Conversely, if $\mathcal C$ is not nowhere dense and in addition is closed under taking sub-graphs and
satisfies some effectivity conditions then FO-model
checking is not FPT on $\mathcal 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 efficiently be coloured "over a class with the type representation property" allows tractable first-order model-checking. Such classes include all classes which are nowhere dense and also all classes of bounded clique-width. This result therefore unifies all known meta-theorems for first-order logic.
Thu, 03 Dec 2009 01:58:51 +0200https://eccc.weizmann.ac.il/report/2009/131