liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On the strength of uniqueness quantification in primitive positive formulas
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Independent researcher.
2019 (English)In: Proceedings of the 44th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl – Leibniz-Zentrum für Informatik , 2019Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Schloss Dagstuhl – Leibniz-Zentrum für Informatik , 2019.
Series
Leibniz International Proceedings in Informatics, ISSN 1868-8969 ; 138
Keywords [en]
Primitive positive definitions; clone theory; constraint satisfaction problems
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-171247DOI: 10.4230/LIPIcs.MFCS.2019.36Scopus ID: 2-s2.0-85071748717ISBN: 978-3-95977-117-7 (print)OAI: oai:DiVA.org:liu-171247DiVA, id: diva2:1500238
Conference
International Symposium on Mathematical Foundations of Computer Science (MFCS), Aachen Germany, August 26-30, 2019
Available from: 2020-11-11 Created: 2020-11-11 Last updated: 2025-11-17Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Lagerkvist, Victor

Search in DiVA

By author/editor
Lagerkvist, Victor
By organisation
Software and SystemsFaculty of Science & Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 43 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf