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

Reduction of (11) to a collection of Boolean axioms is best described by an example. The parity constraint is equivalent to

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 is a
graph, where each node in 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 is a
node of the graph that is labeled with a value and the edges
incident on are labeled with literals
, we add to our theory the Boolean version of
the clause

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 as well. If 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.