2026-07-26T03:15:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10980 2024-03-06T10:46:58Z ddc:004 open_access

On the Strength of Uniqueness Quantification in Primitive Positive Formulas Lagerkvist, Victor Nordh, Gustav Primitive positive definitions clone theory constraint satisfaction problems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Victor Lagerkvist and Gustav Nordh 2019 Is Part Of LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2019.36 urn:nbn:de:0030-drops-109808 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.36 eng https://creativecommons.org/licenses/by/3.0/legalcode