Cookies

We use cookies to ensure that we give you the best experience on our website. You can change your cookie settings at any time. Otherwise, we'll assume you're OK to continue.

Durham University

Research & business

View Profile

Publication details for Dr Barnaby Martin

Madelaine, Florent R. & Martin, Barnaby D. (2018). On the Complexity of the Model Checking Problem. SIAM Journal on Computing 47(3): 769-797.

Author(s) from Durham

Abstract

The complexity of the model checking problem for various fragments of first-order
logic (FO) has attracted much attention over the last two decades, in particular for the fragment
induced by ∃ and ∧ and that induced by ∀, ∃, and ∧, which are better known as the constraint
satisfaction problem and the quantified constraint satisfaction problem, respectively. The former was
conjectured to follow a dichotomy between P and NP-complete by Feder and Vardi [SIAM J. Comput.,
28 (1998), pp. 57–104]. For the latter, there are several partial trichotomy results between P,
NP-complete, and Pspace-complete, and Chen [Meditations on quantified constraint satisfaction, in
Logic and Program Semantics, Springer, Heidelberg, 2012, pp. 35–49] ventured a conjecture regarding
Pspace-completeness vs. membership in NP in the presence of constants. We give a comprehensive
account of the whole field of the complexity of model checking similar syntactic fragments of FO.
The above two fragments are in fact the only ones for which there is currently no known complexity
classification. Indeed, we consider all other similar syntactic fragments of FO, induced by the
presence or absence of quantifiers and connectives, and fully classify the complexities of the parameterization
of the model-checking problem by a finite model D, that is, the expression complexities
for certain finite D. Perhaps surprisingly, we show that for most of these fragments, “tractability”
is witnessed by a generic solving algorithm which uses quantifier relativization. Our classification
methodology relies on tailoring suitably the algebraic approach pioneered by Jeavons, Cohen, and
Gyssens [J. ACM, 44 (1997), pp. 527–548] for the constraint satisfaction problem and by B¨orner
et al. [Inform. and Comput., 207 (2009), pp. 923–944] for the quantified constraint satisfaction
problem. Most fragments under consideration can be relatively easily classified, either directly or
using Schaefer’s dichotomy theorems for SAT and QSAT, with the notable exception of the positive
equality-free fragment induced by ∃, ∀, ∧, and ∨. This outstanding fragment can also be classified
and enjoys a tetrachotomy: according to the model, the corresponding model checking problem is
either tractable, NP-complete, co-NP-complete, or Pspace-complete.