On the complexity of the model checking problem Florent Madelaine and Malika More LIMOS, CNRS
The apparently benign task of checking whether a finite structure models a given sentence from first order logic (FO) and how efficient it might be to run this task on a computer reveals a vivid realm at the interface between computer science and mathematics mixing numerous and diverse fields.
For example, the model checking of a primitive positive sentence (a first-order sentence using only ∃ and ∧) is better known as the Conjunctive Query Containment in Database theory; it can be recast as the existence of a homomorphism between two structures which is a well studied extension of Graph Colouring in Combinatorics ; it is nothing else than a Constraint Satisfaction Problem popular in the Artificial Intelligence community. Perhaps more surprisingly its complexity is governed by algebraic properties of the model from Universal Algebra studied in Clone theory. The dichotomy conjecture first proposed by Feder and Vardi in the early nineties stipulates that according to the model this problem is either tractable (solvable in Polynomial time) or intractable (NP-complete). Around January 2017 three independent proofs have been proposed for this conjecture. We will give a personal view of this field by focusing on fragments of first order logic where again algebra plays a prominent role in understanding and studying the complexity of the model checking problem. These syntactic fragments will be defined by selecting allowed symbols among the following ∀ ∃ ∀ ∨ ∧ ¬ ≠ =. There are no specific prerequisites. The tutorial will be divided in three sessions detailed hereafter.
I. Constraint Satisfaction Problem and the dichotomy conjecture
We will briefly recall the context from Complexity theory (P vs NP, Ladners's theorem) before introducing formally the dichotomy conjecture. So, we focus in this session on the complexity of the model checking of a given primitive positive sentence (fragment ∃ ∧) when parameterised by the model, a problem known as the constraint satisfaction problem (CSP). We will in fact concentrate on the special case when the model has only two elements, which amounts to a variant of propositional Satisfiability (SAT) and sketch the proof of its dichotomy -- this is a result know as Schaefer's dichotomy. Methodologically, the proof relies on a non trivial case analysis that amounts to finding the border between tractable and intractable cases on an underlying algebraic object known as Post's lattice. We will explain in some details why this is the case. In particular, it will be quite illuminating to see how preservation of the model under certain well behaved Boolean functions will make complete certain well known incomplete algorithms. If times allow, we will conclude this session with glimpses of the proofs of more general partial results supporting the dichotomy conjecture. II. what about other fragments of FO?
Bounded model checking from verification is often reduced to the satisfiability problem of quantified Boolean sentences (QBF) that is propositional sentences with variables that are either existential or universal. Many Sat solvers go beyond instances in conjunctive normal form (CNF) and allow some disjunction. This motivates us to investigate fragments of FO allowing the universal quantifier or the disjunction as a connective. Another more prosaic motivation is that studying a fragment of FO that is very expressive will limit the number of cases to study and one might obtain a complexity classification that is still rather elusive in the case of more restricted fragments of FO. |
We will briefly recall the complexity context when one throws universal quantifiers to the mix (Alternating Turing machines, Pspace). We will show that some fragments of FO such as primitive positive first order logic with disequalities (fragment ∃ ∧ ≠) can be classified as corollaries of Schaefer's theorem.
With the exception of these and the fragment corresponding to CSP and its universal extension the QCSP, all other fragments can be classified and exhibit a strange behaviour : tractability is not explained by complicated algorithms but rather by very simple logical properties of the model, namely that a type of quantifier can be relativised to a specific constant of the model.
We will discuss in particular the case of equality free positive first-order logic (fragment ∃ ∀ ∧ ∨) a fragment for which one obtains a tetrachotomy governed by the surjective hyper endormorphisms of the model.
III. Quantified CSP, some progress for the last remaining open case
If one assumes that one of the recent proof proposed for the dichotomy conjecture is correct, there is a single fragment for which the complexity is not classified, namely positive Horn (fragment ∃ ∀ ∧). The model checking problem known as the QCSP is to the CSP what QBF (or QSAT) is to SAT. Some partial results seem to suggest that for a given model the QCSP is either as hard as the general problem (Pspace-complete) or of the same complexity as a hard CSP (NP-complete) or tractable (polynomial time solvable). That is QCSP would follow a trichotomy between Pspace complete, NP-complete and P. The drop in complexity from Pspace to NP seems to be explained also by a slightly more advanced form of relativisation of the universal quantifiers, best explained in terms of restricted games and interpolation of complete Skolem functions from families of partial ones. One natural example known as the collapsibility property enjoyed by some models amounts to the case when it suffices to check the cases where all universal variables of the sentence but a bounded number take a constant value known in advance. Bibliography
Related Surveys
Credits
Back to the 6th Universal Logic School ! | ||||
