Document Open Access Logo

Fixed-Template Promise Model Checking Problems

Authors Kristina Asimi, Libor Barto , Silvia Butti

PDF
Thumbnail PDF

File

LIPIcs.CP.2022.2.pdf
  • Filesize: 0.81 MB
  • 17 pages

Document Identifiers

Author Details

Kristina Asimi
  • Department of Algebra, Faculty of Mathematics and Physics, Charles University, Prague, Czechia
Libor Barto
  • Department of Algebra, Faculty of Mathematics and Physics, Charles University, Prague, Czechia
Silvia Butti
  • Department of Information and Communication Technologies, Universitat Pompeu Fabra, Barcelona, Spain

Funding

Kristina Asimi and Libor Barto have received funding from the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme (Grant Agreement No. 771005, CoCoSym). Silvia Butti was supported by a MICCIN grant PID2019-109137GB-C22 and by a fellowship from "la Caixa" Foundation (ID 100010434). The fellowship code is LCF/BQ/DI18/11660056. This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 713673.

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.CP.2022.2

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • Model Checking Problem
  • First-Order Logic
  • Promise Constraint Satisfaction Problem
  • Multi-Homomorphism

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Per Austrin, Venkatesan Guruswami, and Johan Håstad. (2+ε)-Sat is NP-hard. SIAM J. Comput., 46(5):1554-1573, 2017. URL: https://doi.org/10.1137/15M1006507.
  2. Libor Barto, Jakub Bulín, Andrei A. Krokhin, and Jakub Opršal. Algebraic approach to promise constraint satisfaction. J. ACM, 68(4):28:1-28:66, 2021. URL: https://doi.org/10.1145/3457606.
  3. Libor Barto, Andrei Krokhin, and Ross Willard. Polymorphisms, and How to Use Them. In Andrei Krokhin and Stanislav Živný, editors, The Constraint Satisfaction Problem: Complexity and Approximability, volume 7 of Dagstuhl Follow-Ups, pages 1-44. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2017. URL: https://doi.org/10.4230/DFU.Vol7.15301.1.
  4. Ferdinand Börner. Basics of Galois Connections. In Nadia Creignou, Phokion G. Kolaitis, and Heribert Vollmer, editors, Complexity of Constraints - An Overview of Current Research Themes [Result of a Dagstuhl Seminar], volume 5250 of Lecture Notes in Computer Science, pages 38-67. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-92800-3_3.
  5. Joshua Brakensiek and Venkatesan Guruswami. Promise Constraint Satisfaction: Structure Theory and a Symmetric Boolean Dichotomy. In Proceedings of the Twenty-Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA'18, pages 1782-1801, Philadelphia, PA, USA, 2018. Society for Industrial and Applied Mathematics. URL: https://doi.org/10.1137/1.9781611975031.117.
  6. A. A. Bulatov. A dichotomy theorem for nonuniform CSPs. In 2017 IEEE 58th Annual Symposium on Foundations of Computer Science (FOCS), pages 319-330, October 2017. URL: https://doi.org/10.1109/FOCS.2017.37.
  7. Catarina Carvalho and Barnaby Martin. The lattice and semigroup structure of multipermutations. International Journal of Algebra and Computation, 0(0):1-25, 2021. URL: https://doi.org/10.1142/S0218196722500096.
  8. Hubie Chen. Meditations on quantified constraint satisfaction. In Robert L. Constable and Alexandra Silva, editors, Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, volume 7230 of Lecture Notes in Computer Science, pages 35-49. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-29485-3_4.
  9. Venkatesan Guruswami and Euiwoong Lee. Strong inapproximability results on balanced rainbow-colorable hypergraphs. Comb., 38(3):547-599, 2018. URL: https://doi.org/10.1007/s00493-016-3383-0.
  10. Nancy Lynch. Log space recognition and translation of parenthesis languages. J. ACM, 24(4):583-590, October 1977. URL: https://doi.org/10.1145/322033.322037.
  11. Florent Madelaine and Barnaby Martin. The complexity of positive first-order logic without equality. ACM Trans. Comput. Logic, 13(1), January 2012. URL: https://doi.org/10.1145/2071368.2071373.
  12. Florent R. Madelaine and Barnaby Martin. A tetrachotomy for positive first-order logic without equality. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 311-320. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/LICS.2011.27.
  13. Florent R. Madelaine and Barnaby Martin. On the complexity of the model checking problem. SIAM J. Comput., 47(3):769-797, 2018. URL: https://doi.org/10.1137/140965715.
  14. Barnaby Martin. First-order model checking problems parameterized by the model. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors, Logic and Theory of Algorithms, 4th Conference on Computability in Europe, CiE 2008, Athens, Greece, June 15-20, 2008, Proceedings, volume 5028 of Lecture Notes in Computer Science, pages 417-427. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-69407-6_45.
  15. Barnaby Martin. The lattice structure of sets of surjective hyper-operations. In David Cohen, editor, Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, volume 6308 of Lecture Notes in Computer Science, pages 368-382. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15396-9_31.
  16. Barnaby Martin. Quantified Constraints in Twenty Seventeen. In Andrei Krokhin and Stanislav Živný, editors, The Constraint Satisfaction Problem: Complexity and Approximability, volume 7 of Dagstuhl Follow-Ups, pages 327-346. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2017. URL: https://doi.org/10.4230/DFU.Vol7.15301.327.
  17. Barnaby Martin and Jos Martin. The complexity of positive first-order logic without equality II: the four-element case. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 426-438. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_33.
  18. Dmitriy Zhuk. A proof of the CSP dichotomy conjecture. J. ACM, 67(5):30:1-30:78, August 2020. URL: https://doi.org/10.1145/3402029.
  19. Dmitriy Zhuk and Barnaby Martin. QCSP monsters and the demise of the chen conjecture. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 91-104. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384232.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact