CNF Encodings of Parity

TL;DR

This paper establishes new lower bounds on the size and width of CNF encodings for the parity function, showing limitations even with auxiliary variables, and uses the Satisfiability Coding Lemma for proofs.

Contribution

It provides the first tight lower bounds on clause count and width for CNF encodings of parity with auxiliary variables, advancing theoretical understanding.

Findings

Lower bound of rac{2^{n/(s+1)}}{n} on clauses with s auxiliary variables

Minimum clauses at least 3n

Bounds derived using the Satisfiability Coding Lemma

Abstract

The minimum number of clauses in a CNF representation of the parity function $x_1 \oplus x_2 \oplus \dotsb \oplus 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 \ge \Omega\left(2^{n/(s+1)}/n\right)$ and $k \ge 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, Pudlak, and Zane.