2026-07-26T02:32:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16845 2024-03-06T10:58:29Z ddc:004 open_access

CNF Encodings of Parity Emdin, Gregory Kulikov, Alexander S. Mihajlin, Ivan Slezkin, Nikita encoding parity lower bounds circuits CNF 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gregory Emdin and Alexander S. Kulikov and Ivan Mihajlin and Nikita Slezkin 2022 Is Part Of LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2022.47 urn:nbn:de:0030-drops-168455 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.47 eng https://creativecommons.org/licenses/by/4.0/legalcode