2026-09-29T12:41:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16631 2026-09-23T16:28:46Z ddc:004 open_access

Fixed-Template Promise Model Checking Problems Asimi, Kristina Barto, Libor Butti, Silvia Model Checking Problem First-Order Logic Promise Constraint Satisfaction Problem Multi-Homomorphism 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 ℒ 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 ℒ, 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., ℒ = {∃,∧,∨}, and we prove some upper and lower bounds for the positive equality-free fragment, ℒ = {∃,∀,∧,∨}. The partial results are sufficient, e.g., for all extensions of the latter fragment. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Kristina Asimi and Libor Barto and Silvia Butti 2022 Is Part Of LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2022.2 urn:nbn:de:0030-drops-166310 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.2 eng https://creativecommons.org/licenses/by/4.0/legalcode