Promise Model Checking Problems

Kristina Asimi ( Durham University )

The fixed-template constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive first-order sentence is true in a fixed structure (also called model).

In this talk, I will present joint work in which we study a class of problems that generalises the CSP simultaneously in two directions: we fix a set $L$ of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from $L$, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We call such a problem a Promise Model Checking Problem. We classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic, i.e., $L = \{\exists,\land,\lor\}$, and we prove some upper and lower bounds for the positive equality-free fragment, $L = \{\exists,\forall,\land,\lor\}$.

In the final part of the talk, I will introduce recent work on Model Checking Problem over the positive equality-free fragment, which also provides the complexity of a specific Promise Model Checking Problem not covered in our paper.