Document Open Access Logo

CNF Encodings of Parity

Authors Gregory Emdin, Alexander S. Kulikov , Ivan Mihajlin, Nikita Slezkin

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2022.47.pdf
  • Filesize: 0.72 MB
  • 12 pages

Document Identifiers

Related Versions

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Gregory Emdin
  • St. Petersburg State University, Russia
Alexander S. Kulikov
  • Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences, Russia
  • St. Petersburg State University, Russia
Ivan Mihajlin
  • Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences, Russia
Nikita Slezkin
  • Steklov Mathematical Institute at St. Petersburg, Russian Academy of Sciences, Russia

Acknowledgements

Research is partially supported by Huawei (grant TC20211214628).

References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. William J. Masek. Some NP-complete set covering problems. Unpublished Manuscript, 1979. Google Scholar
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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. Google Scholar
  13. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact