Fixed-Template Promise Model Checking Problems

TL;DR

This paper investigates the computational complexity of fixed-template promise model checking problems within certain fragments of first-order logic, providing classifications and bounds for these problems.

Contribution

It introduces a generalized framework for fixed-template CSPs with quantifier and connective restrictions, and classifies their complexity for specific logical fragments.

Findings

Classified complexity of the existential positive equality-free fragment.

Established upper and lower bounds for the positive equality-free fragment.

Provided partial results applicable to all extensions of the studied fragments.

Abstract

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). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set $\mathcal{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 $\mathcal{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 classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic, i.e., $\mathcal{L} = \{\exists,\land,\lor\}$, and we prove some upper and lower bounds for the positive equality-free fragment, $\mathcal{L} = \{\exists,\forall,\land,\lor\}$. The partial results are sufficient, e.g., for all extensions of the latter fragment.