Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2022.2
URN: urn:nbn:de:0030-drops-166310
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16631/
Asimi, Kristina ; Barto, Libor ; Butti, Silvia
Fixed-Template Promise Model Checking Problems
| pdf-format: |
|
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 ℒ 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.
BibTeX - Entry
@InProceedings{asimi_et_al:LIPIcs.CP.2022.2,
author = {Asimi, Kristina and Barto, Libor and Butti, Silvia},
title = {{Fixed-Template Promise Model Checking Problems}},
booktitle = {28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
pages = {2:1--2:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-240-2},
ISSN = {1868-8969},
year = {2022},
volume = {235},
editor = {Solnon, Christine},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16631},
URN = {urn:nbn:de:0030-drops-166310},
doi = {10.4230/LIPIcs.CP.2022.2},
annote = {Keywords: Model Checking Problem, First-Order Logic, Promise Constraint Satisfaction Problem, Multi-Homomorphism}
}
| Keywords: | Model Checking Problem, First-Order Logic, Promise Constraint Satisfaction Problem, Multi-Homomorphism | |
| Seminar: | 28th International Conference on Principles and Practice of Constraint Programming (CP 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 23.07.2022 |
