DROPS

Document

DOI: 10.4230/LIPIcs.MFCS.2022.47

CNF Encodings of Parity

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

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

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

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)

Copy BibTex To Clipboard

@InProceedings{emdin_et_al:LIPIcs.MFCS.2022.47,
  author =	{Emdin, Gregory and Kulikov, Alexander S. and Mihajlin, Ivan and Slezkin, Nikita},
  title =	{{CNF Encodings of Parity}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{47:1--47:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.47},
  URN =		{urn:nbn:de:0030-drops-168455},
  doi =		{10.4230/LIPIcs.MFCS.2022.47},
  annote =	{Keywords: encoding, parity, lower bounds, circuits, CNF}
}

Search Results

Documents authored by Emdin, Gregory

CNF Encodings of Parity

Abstract

Cite as

Thanks for your feedback!

Could not send message