Document Open Access Logo

On the Strength of Uniqueness Quantification in Primitive Positive Formulas

Authors Victor Lagerkvist, Gustav Nordh

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.36.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Author Details

Victor Lagerkvist
  • Department of Computer and Information Science, Linköping University, Linköping, Sweden
Gustav Nordh
  • Independent researcher, Hällekis, Sweden

Acknowledgements

We thank Andrei Bulatov for helpful discussions concerning the topic of the paper, and the anonymous reviewers for their constructive feedback.

Cite AsGet BibTex

Victor Lagerkvist and Gustav Nordh. On the Strength of Uniqueness Quantification in Primitive Positive Formulas. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 36:1-36:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.MFCS.2019.36

Abstract

Uniqueness quantification (Exists!) is a quantifier in first-order logic where one requires that exactly one element exists satisfying a given property. In this paper we investigate the strength of uniqueness quantification when it is used in place of existential quantification in conjunctive formulas over a given set of relations Gamma, so-called primitive positive definitions (pp-definitions). We fully classify the Boolean sets of relations where uniqueness quantification has the same strength as existential quantification in pp-definitions and give several results valid for arbitrary finite domains. We also consider applications of Exists!-quantified pp-definitions in computer science, which can be used to study the computational complexity of problems where the number of solutions is important. Using our classification we give a new and simplified proof of the trichotomy theorem for the unique satisfiability problem, and prove a general result for the unique constraint satisfaction problem. Studying these problems in a more rigorous framework also turns out to be advantageous in the context of lower bounds, and we relate the complexity of these problems to the exponential-time hypothesis.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Discrete mathematics
Keywords
  • Primitive positive definitions
  • clone theory
  • constraint satisfaction problems

Metrics

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

Related Versions

References

  1. L. Barto, A. Krokhin, and R. Willard. Polymorphisms, and How to Use Them. In Andrei Krokhin and Stanislav Zivny, 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. Google Scholar
  2. A. Blass and Y. Gurevich. On the unique satisfiability problem. Information and Control, 55(1):80-88, 1982. Google Scholar
  3. V. G. Bodnarchuk, L. A. Kaluzhnin, V. N. Kotov, and B. A. Romov. Galois theory for Post algebras. I. Cybernetics, 5:243-252, 1969. Google Scholar
  4. V. G. Bodnarchuk, L. A. Kaluzhnin, V. N. Kotov, and B. A. Romov. Galois theory for Post algebras. II. Cybernetics, 5:531-539, 1969. Google Scholar
  5. E. Böhler, N. Creignou, S. Reith, and H. Vollmer. Playing with Boolean Blocks, Part I: Post’s Lattice with Applications to Complexity Theory. ACM SIGACT-Newsletter, 34(4):38-52, 2003. Google Scholar
  6. A. Bulatov. A dichotomy theorem for nonuniform CSPs. In Proceedings of the 58th Annual Symposium on Foundations of Computer Science (FOCS-2017). IEEE Computer Society, 2017. Google Scholar
  7. N. Creignou and M. Hermann. Complexity of Generalized Satisfiability Counting Problems. Information and Computation, 125(1):1-12, 1996. Google Scholar
  8. N. Creignou, S. Khanna, and M. Sudan. Complexity classifications of Boolean constraint satisfaction problems. SIAM Monographs on Discrete Mathematics and Applications, 2001. Google Scholar
  9. N. Creignou, P. Kolaitis, and B. Zanuttini. Structure identification of Boolean relations and plain bases for co-clones. Journal of Computer and System Sciences, 74(7):1103-1115, November 2008. Google Scholar
  10. N. Creignou and H. Vollmer. Boolean Constraint Satisfaction Problems: When Does Post’s Lattice Help? In N. Creignou, P. G. Kolaitis, and H. Vollmer, editors, Complexity of Constraints, volume 5250 of Lecture Notes in Computer Science, pages 3-37. Springer Berlin Heidelberg, 2008. Google Scholar
  11. D. Geiger. Closed Systems of Functions and Predicates. Pacific Journal of Mathematics, 27(1):95-100, 1968. Google Scholar
  12. R. Impagliazzo and R. Paturi. On the Complexity of k-SAT. Journal of Computer and System Sciences, 62(2):367-375, 2001. Google Scholar
  13. P. Jeavons. On The Algebraic Structure Of Combinatorial Problems. Theoretical Computer Science, 200:185-204, 1998. Google Scholar
  14. P. Jeavons, D. Cohen, and M. Gyssens. A unifying framework for tractable constraints. In Proceedings of the First International Conference in Principles and Practice of Constraint Programming (CP-1995), pages 276-291, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  15. L. Juban. Dichotomy Theorem for the Generalized Unique Satisfiability Problem. In Proceedings of the 12th International Symposium of Fundamentals of Computation Theory (FCT-1999), volume 1684 of Lecture Notes in Computer Science, pages 327-337. Springer, 1999. Google Scholar
  16. D. Kavvadias and M. Sideri. The Inverse Satisfiability Problem. SIAM Journal on Computing, 28:152-163, 1998. Google Scholar
  17. V. Lagerkvist. Weak bases of Boolean co-clones. Information Processing Letters, 114(9):462-468, 2014. Google Scholar
  18. V. Lagerkvist. Strong Partial Clones and the Complexity of Constraint Satisfaction Problems: Limitations and Applications. PhD thesis, Linköping University, The Institute of Technology, 2016. Google Scholar
  19. V. Lagerkvist and G. Nordh. On the Strength of Uniqueness Quantification in Primitive Positive Formulas. ArXiv e-prints, June 2019. URL: http://arxiv.org/abs/1906.07031.
  20. V. Lagerkvist and B. Roy. A Dichotomy Theorem for the Inverse Satisfiability Problem. In Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS-2017), volume 93, pages 39:39-39:14, 2018. Google Scholar
  21. D. Lau. Function Algebras on Finite Sets: Basic Course on Many-Valued Logic and Clone Theory (Springer Monographs in Mathematics). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006. Google Scholar
  22. G. Nordh and B. Zanuttini. Frozen Boolean Partial Co-clones. In Proceedings of the 39th International Symposium on Multiple-Valued Logic (ISMVL-2009), pages 120-125, 2009. URL: https://doi.org/10.1109/ISMVL.2009.10.
  23. C.H. Papadimitriou and M. Yannakakis. The complexity of facets (and some facets of complexity). Journal of Computer and System Sciences, 28(2):244-259, 1984. Google Scholar
  24. E. Post. The two-valued iterative systems of mathematical logic. Annals of Mathematical Studies, 5:1-122, 1941. Google Scholar
  25. S. Reith and K. W. Wagner. The Complexity of Problems Defined by Boolean Circuits. In Proceedings International Conference Mathematical Foundation of Informatics (MFI-1999), pages 25-28, 1999. Google Scholar
  26. B.A. Romov. The algebras of partial functions and their invariants. Cybernetics, 17(2):157-167, 1981. Google Scholar
  27. H. Schnoor and I. Schnoor. Partial Polymorphisms and Constraint Satisfaction Problems. In N. Creignou, P. G. Kolaitis, and H. Vollmer, editors, Complexity of Constraints, volume 5250 of Lecture Notes in Computer Science, pages 229-254. Springer Berlin Heidelberg, 2008. Google Scholar
  28. D. Zhuk. The Proof of CSP Dichotomy Conjecture. In Proceedings of the 58th Annual Symposium on Foundations of Computer Science (FOCS-2017). IEEE Computer Society, 2017. Google Scholar
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 Imprint Privacy Contact