DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2019.36

On the Strength of Uniqueness Quantification in Primitive Positive Formulas

Authors: Victor Lagerkvist and Gustav Nordh

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{lagerkvist_et_al:LIPIcs.MFCS.2019.36,
  author =	{Lagerkvist, Victor and Nordh, Gustav},
  title =	{{On the Strength of Uniqueness Quantification in Primitive Positive Formulas}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{36:1--36:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.36},
  URN =		{urn:nbn:de:0030-drops-109808},
  doi =		{10.4230/LIPIcs.MFCS.2019.36},
  annote =	{Keywords: Primitive positive definitions, clone theory, constraint satisfaction problems}
}

Search Results

Documents authored by Nordh, Gustav

On the Strength of Uniqueness Quantification in Primitive Positive Formulas

Abstract

Cite as

Thanks for your feedback!

Could not send message