DROPS

Document

DOI: 10.4230/LIPIcs.CP.2022.2

Fixed-Template Promise Model Checking Problems

Authors: Kristina Asimi, Libor Barto, and Silvia Butti

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

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.

Cite as

Kristina Asimi, Libor Barto, and Silvia Butti. Fixed-Template Promise Model Checking Problems. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.CP.2022.2},
  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}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2021.11

Finitely Tractable Promise Constraint Satisfaction Problems

Authors: Kristina Asimi and Libor Barto

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract

The Promise Constraint Satisfaction Problem (PCSP) is a generalization of the Constraint Satisfaction Problem (CSP) that includes approximation variants of satisfiability and graph coloring problems. Barto [LICS '19] has shown that a specific PCSP, the problem to find a valid Not-All-Equal solution to a 1-in-3-SAT instance, is not finitely tractable in that it can be solved by a trivial reduction to a tractable CSP, but such a CSP is necessarily over an infinite domain (unless P=NP). We initiate a systematic study of this phenomenon by giving a general necessary condition for finite tractability and characterizing finite tractability within a class of templates - the "basic" tractable cases in the dichotomy theorem for symmetric Boolean PCSPs allowing negations by Brakensiek and Guruswami [SODA'18].

Cite as

Kristina Asimi and Libor Barto. Finitely Tractable Promise Constraint Satisfaction Problems. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 11:1-11:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{asimi_et_al:LIPIcs.MFCS.2021.11,
  author =	{Asimi, Kristina and Barto, Libor},
  title =	{{Finitely Tractable Promise Constraint Satisfaction Problems}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.11},
  URN =		{urn:nbn:de:0030-drops-144519},
  doi =		{10.4230/LIPIcs.MFCS.2021.11},
  annote =	{Keywords: Constraint satisfaction problems, promise constraint satisfaction, Boolean PCSP, polymorphism, finite tractability, homomorphic relaxation}
}

Search Results

Documents authored by Asimi, Kristina

Fixed-Template Promise Model Checking Problems

Abstract

Cite as

Finitely Tractable Promise Constraint Satisfaction Problems

Abstract

Cite as

Thanks for your feedback!

Could not send message