  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.
