On the Strength of Uniqueness Quantification in Primitive Positive Formulas
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.
Primitive positive definitions
clone theory
constraint satisfaction problems
Mathematics of computing~Discrete mathematics
36:1-36:15
Regular Paper
https://arxiv.org/abs/1906.07031
We thank Andrei Bulatov for helpful discussions concerning the topic of the paper, and the anonymous reviewers for their constructive feedback.
Victor
Lagerkvist
Victor Lagerkvist
Department of Computer and Information Science, Linköping University, Linköping, Sweden
Gustav
Nordh
Gustav Nordh
Independent researcher, Hällekis, Sweden
10.4230/LIPIcs.MFCS.2019.36
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.
A. Blass and Y. Gurevich. On the unique satisfiability problem. Information and Control, 55(1):80-88, 1982.
V. G. Bodnarchuk, L. A. Kaluzhnin, V. N. Kotov, and B. A. Romov. Galois theory for Post algebras. I. Cybernetics, 5:243-252, 1969.
V. G. Bodnarchuk, L. A. Kaluzhnin, V. N. Kotov, and B. A. Romov. Galois theory for Post algebras. II. Cybernetics, 5:531-539, 1969.
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.
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.
N. Creignou and M. Hermann. Complexity of Generalized Satisfiability Counting Problems. Information and Computation, 125(1):1-12, 1996.
N. Creignou, S. Khanna, and M. Sudan. Complexity classifications of Boolean constraint satisfaction problems. SIAM Monographs on Discrete Mathematics and Applications, 2001.
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.
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.
D. Geiger. Closed Systems of Functions and Predicates. Pacific Journal of Mathematics, 27(1):95-100, 1968.
R. Impagliazzo and R. Paturi. On the Complexity of k-SAT. Journal of Computer and System Sciences, 62(2):367-375, 2001.
P. Jeavons. On The Algebraic Structure Of Combinatorial Problems. Theoretical Computer Science, 200:185-204, 1998.
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.
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.
D. Kavvadias and M. Sideri. The Inverse Satisfiability Problem. SIAM Journal on Computing, 28:152-163, 1998.
V. Lagerkvist. Weak bases of Boolean co-clones. Information Processing Letters, 114(9):462-468, 2014.
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.
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.
http://arxiv.org/abs/1906.07031
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.
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.
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.
https://doi.org/10.1109/ISMVL.2009.10
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.
E. Post. The two-valued iterative systems of mathematical logic. Annals of Mathematical Studies, 5:1-122, 1941.
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.
B.A. Romov. The algebras of partial functions and their invariants. Cybernetics, 17(2):157-167, 1981.
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.
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.
Victor Lagerkvist and Gustav Nordh
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode