Next: Clique coloring problems Up: Proof Complexity Previous: Pigeonhole problems

### 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,

 (11)

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

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

 (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 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.

Next: Clique coloring problems Up: Proof Complexity Previous: Pigeonhole problems
Matt Ginsberg 2004-02-19