Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #2 to TR09-131 | 19th March 2013 14:53

Parameterized Complexity of First-Order Logic

RSS-Feed




Revision #2
Authors: Anuj Dawar, Stephan Kreutzer
Accepted on: 19th March 2013 14:53
Downloads: 2351
Keywords: 


Abstract:

We 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.


Revision #1 to TR09-131 | 19th March 2013 14:21

Parameterized Complexity of First-Order Logic





Revision #1
Authors: Anuj Dawar, Stephan Kreutzer
Accepted on: 19th March 2013 14:21
Downloads: 2426
Keywords: 


Abstract:

We 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.


Paper:

TR09-131 | 2nd December 2009 19:19

Parameterized Complexity of First-Order Logic





TR09-131
Authors: Stephan Kreutzer, Anuj Dawar
Publication: 3rd December 2009 01:58
Downloads: 4015
Keywords: 


Abstract:

We 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.



ISSN 1433-8092 | Imprint