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}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2022.67

SAT-Based Circuit Local Improvement

Authors: Alexander S. Kulikov, Danila Pechenev, and Nikita Slezkin

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

Abstract

Finding exact circuit size is notoriously hard. Whereas modern computers and algorithmic techniques allow to find a circuit of size seven in the blink of an eye, it may take more than a week to search for a circuit of size thirteen. One of the reasons of this behavior is that the search space is enormous: the number of circuits of size s is s^Θ(s), the number of Boolean functions on n variables is 2^(2ⁿ). In this paper, we explore the following natural heuristic idea for decreasing the size of a given circuit: go through all its subcircuits of moderate size and check whether any of them can be improved by reducing to SAT. This may be viewed as a local search approach: we search for a smaller circuit in a ball around a given circuit. Through this approach, we prove new upper bounds on the circuit size of various symmetric functions. We also demonstrate that some upper bounds that were proved by hand decades ago, can nowadays be found automatically in a few seconds.

Cite as

Alexander S. Kulikov, Danila Pechenev, and Nikita Slezkin. SAT-Based Circuit Local Improvement. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 67:1-67:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kulikov_et_al:LIPIcs.MFCS.2022.67,
  author =	{Kulikov, Alexander S. and Pechenev, Danila and Slezkin, Nikita},
  title =	{{SAT-Based Circuit Local Improvement}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{67:1--67:15},
  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.67},
  URN =		{urn:nbn:de:0030-drops-168659},
  doi =		{10.4230/LIPIcs.MFCS.2022.67},
  annote =	{Keywords: circuits, algorithms, complexity theory, SAT, SAT solvers, heuristics}
}

Search Results

Documents authored by Slezkin, Nikita

CNF Encodings of Parity

Abstract

Cite as

SAT-Based Circuit Local Improvement

Abstract

Cite as

Thanks for your feedback!

Could not send message