CNF Encodings of Symmetric Functions

• Published in: Theory of computing systems 2024-10, Vol.68 (5), p.1291-1311
• Main Authors: Emdin, Gregory, Kulikov, Alexander S., Mihajlin, Ivan, Slezkin, Nikita
• Format: Article
• Language: English
• Subjects: Boolean; Boolean functions; Codes; Coding; Computer Science; Lower bounds; Parity; Theory of Computation
• ISSN: 1432-4350; 1433-0490
• DOI: 10.1007/s00224-024-10168-w

Many Boolean functions that need to be encoded as CNF in practice, have only exponential size CNF representations. To avoid this effect, one usually introduces nondeterministic variables. For example, whereas the minimum number of clauses in a CNF computing the parity function x 1 ⊕ x 2 ⊕ ⋯ ⊕ x n is  2 n - 1 , one can use n - 1 nondeterministic variables to get a CNF encoding with 4 n  clauses. In this paper, we prove tradeoffs between various parameters (the number of clauses, the width of clauses, and the number of nondeterministic variables) of CNF encodings of various symmetric functions. In particular, we show that a folklore way of encoding parity as CNF is provably optimal. We do this by using a tight connection between CNF encodings and depth-3 circuits. This connection shows that CNF encodings is an interesting computational model for Boolean functions: on the one hand, it is routinely used in practice when translating a computational problem to a format acceptable by a SAT solver, on the other hand, lower bounds on the size of CNF encodings imply depth-3 circuit lower bounds.