CNF Encodings of Symmetric Functions

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₁⊕ x₂ ⊕ ⊕ xₙ is~2ⁿ⁻¹, one can use $n-1$ nondeterministic variables to~get a~CNF encoding with $4n$~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~practical 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.