LIPIcs.MFCS.2022.47.pdf
- Filesize: 0.72 MB
- 12 pages
Document
CNF Encodings of Parity
Authors
Alexander S. Kulikov 
,
Nikita Slezkin
-
Part of:
Volume:
47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Mathematical Foundations of Computer Science (MFCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-08-22
File
Document Identifiers
Author Details
- Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences, Russia
- St. Petersburg State University, Russia
Acknowledgements
Research is partially supported by Huawei (grant TC20211214628).
Cite As Get BibTex
Gregory Emdin, Alexander S. Kulikov, Ivan Mihajlin, and Nikita Slezkin. CNF Encodings of Parity. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 47:1-47:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.47
Abstract
The minimum number of clauses in a CNF representation of the parity function x₁ ⊕ x₂ ⊕ … ⊕ x_n is 2^{n-1}. One can obtain a more compact CNF encoding by using non-deterministic variables (also known as guess or auxiliary variables). In this paper, we prove the following lower bounds, that almost match known upper bounds, on the number m of clauses and the maximum width k of clauses: 1) if there are at most s auxiliary variables, then m ≥ Ω(2^{n/(s+1)}/n) and k ≥ n/(s+1); 2) the minimum number of clauses is at least 3n. We derive the first two bounds from the Satisfiability Coding Lemma due to Paturi, Pudlák, and Zane using a tight connection between CNF encodings and depth-3 circuits. In particular, we show that lower bounds on the size of a CNF encoding of a Boolean function imply depth-3 circuit lower bounds for this function.
Subject Classification
ACM Subject Classification
- Theory of computation → Complexity theory and logic
- Theory of computation → Circuit complexity
Keywords
- encoding
- parity
- lower bounds
- circuits
- CNF
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Eric Allender, Lisa Hellerstein, Paul McCabe, Toniann Pitassi, and Michael E. Saks. Minimizing disjunctive normal form formulas and AC⁰ circuits given a truth table. SIAM J. Comput., 38(1):63-84, 2008. URL: https://doi.org/10.1137/060664537.
- Judy Goldsmith, Matthew A. Levy, and Martin Mundhenk. Limited nondeterminism. SIGACT News, 27(2):20-29, 1996. URL: https://doi.org/10.1145/235767.235769.
- Shuichi Hirahara. A duality between depth-three formulas and approximation by depth-two. Electron. Colloquium Comput. Complex., page 92, 2017. URL: https://eccc.weizmann.ac.il/report/2017/092.
- Stasys Jukna. Boolean Function Complexity - Advances and Frontiers, volume 27 of Algorithms and combinatorics. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-24508-4.
- Petr Kucera, Petr Savický, and Vojtech Vorel. A lower bound on CNF encodings of the at-most-one constraint. Theor. Comput. Sci., 762:51-73, 2019. URL: https://doi.org/10.1016/j.tcs.2018.09.003.
-
William J. Masek. Some NP-complete set covering problems. Unpublished Manuscript, 1979.
- Hiroki Morizumi. Lower bounds for the size of nondeterministic circuits. In Dachuan Xu, Donglei Du, and Ding-Zhu Du, editors, Computing and Combinatorics - 21st International Conference, COCOON 2015, Beijing, China, August 4-6, 2015, Proceedings, volume 9198 of Lecture Notes in Computer Science, pages 289-296. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21398-9_23.
- Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. Chic. J. Theor. Comput. Sci., 1999, 1999. URL: http://cjtcs.cs.uchicago.edu/articles/1999/11/contents.html.
- Steven David Prestwich. SAT problems with chains of dependent variables. Discret. Appl. Math., 130(2):329-350, 2003. URL: https://doi.org/10.1016/S0166-218X(02)00410-9.
- Steven David Prestwich. CNF encodings. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 75-97. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-75.
- Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In Peter van Beek, editor, Principles and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005, Sitges, Spain, October 1-5, 2005, Proceedings, volume 3709 of Lecture Notes in Computer Science, pages 827-831. Springer, 2005. URL: https://doi.org/10.1007/11564751_73.
-
G. S. Tsejtin. On the complexity of derivation in propositional calculus. Semin. Math., V. A. Steklov Math. Inst., Leningrad 8, 115-125 (1970); translation from Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 8, 234-259 (1968)., 1968.
- Leslie G. Valiant. Graph-theoretic arguments in low-level complexity. In Jozef Gruska, editor, Mathematical Foundations of Computer Science 1977, 6th Symposium, Tatranska Lomnica, Czechoslovakia, September 5-9, 1977, Proceedings, volume 53 of Lecture Notes in Computer Science, pages 162-176. Springer, 1977. URL: https://doi.org/10.1007/3-540-08353-7_135.