On the complexity of the model checking problem

TL;DR

This paper investigates the complexity classifications of various fragments of first-order logic model checking, revealing a tetrachotomy for the positive equality free fragment and algebraic characterizations for complexity.

Contribution

It provides a comprehensive complexity classification for the positive equality free fragment, including a tetrachotomy and algebraic characterizations, filling a major gap in the field.

Findings

The positive equality free fragment has a tetrachotomy: tractable, NP-complete, co-NP-complete, or Pspace-complete.

A generic solving algorithm with quantifier relativisation witnesses complexity drops.

Algebraic properties, like specific surjective hyper-operations, characterize complexity.

Abstract

The model checking problem for various fragments of first-order logic has attracted much attention over the last two decades: in particular, for the primitive positive and the positive Horn fragments, which are better known as the constraint satisfaction problem and the quantified constraint satisfaction problem, respectively. These two fragments are in fact the only ones for which there is currently no known complexity classification. All other syntactic fragments can be easily classified, either directly or using Schaefer's dichotomy theorems for SAT and QSAT, with the exception of the positive equality free fragment. 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. Moreover, the complexity drop is always witnessed by a generic solving algorithm which uses quantifier relativisation. Furthermore, its complexity is characterised by algebraic means: the presence or absence of specific surjective hyper-operations among those that preserve the model characterise the complexity.