eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-08-20
36:1
36:15
10.4230/LIPIcs.MFCS.2019.36
article
On the Strength of Uniqueness Quantification in Primitive Positive Formulas
Lagerkvist, Victor
1
Nordh, Gustav
2
Department of Computer and Information Science, Linköping University, Linköping, Sweden
Independent researcher, Hällekis, Sweden
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol138-mfcs2019/LIPIcs.MFCS.2019.36/LIPIcs.MFCS.2019.36.pdf
Primitive positive definitions
clone theory
constraint satisfaction problems