Parity problems

By a parity problem, we will mean a collection of axioms specifying the parity of sets of inputs. So we will write, for example,

$$x_1\oplus\cdots\oplus x_n = 1$$ (11)

to indicates that an odd number of the $x_i$ are true; a right hand side of zero would indicate that an even number were true. The $\oplus$ here indicates exclusive or.

Reduction of (11) to a collection of Boolean axioms is best described by an example. The parity constraint $x\oplus y \oplus z=1$ is equivalent to

$$\begin{eqnarray*} & x\vee y\vee z & \\ & x \vee \neg y \vee \neg z & \\ & \neg x \vee y \vee \neg z & \\ & \neg x \vee \neg y \vee z & \end{eqnarray*}$$

In general, the number of Boolean axioms needed is exponential in the length of the parity clause (11), but for clauses of a fixed length, the number of axioms is obviously fixed as well.

For the proof complexity result of interest, suppose that $G$ is a graph, where each node in $G$ will correspond to a clause and each edge to a literal. We label the edges with distinct literals, and label each node of the graph with a zero or a one. Now if $n$ is a node of the graph that is labeled with a value $v_n$ and the edges $e_{1n},\dots,e_{i(n),n}$ incident on $n$ are labeled with literals $l_{1n},\dots,l_{i(n),n}$, we add to our theory the Boolean version of the clause

$$l_{1n}\oplus\cdots\oplus l_{i(n),n} = v_n$$ (12)

Since every edge connects two nodes, every literal in the theory appears exactly twice in axioms of the form (12). Adding all of these constraints therefore produces a value that is equivalent to zero mod 2 and must be equal to $\sum_n v_n$ as well. If $\sum_n v_n$ is odd, the theory is unsatisfiable. Tseitin's Tseitin:complexity principal result is to show that this unsatisfiability cannot in general be proven in a number of resolution steps polynomial in the size of the Boolean encoding.