Proof Complexity

We have already shown in Proposition 3.2 that pseudo-Boolean or cardinality-based axiomatizations can produce polynomially sized proofs of the pigeonhole problem. It is also known that these methods do not lead to polynomially sized proofs of the clique coloring problem [Bonet, Pitassi, RazBonet et al.1997,Kraj'icekKraj'icek1997,PudlakPudlak1997]. The situation with regard to parity constraints is a bit more interesting.

Let us first point out that it is possible to capture parity constraints, or modularity constraints generally in a pseudo-Boolean setting:

Definition 3.18   A modularity constraint is a constraint $c$ of the form

$$\sum_i w_i l_i~\equiv n (\mbox{\rm mod}\ m)$$ (33)

for positive integers $w_i$, $n$ and $m$.

In the remainder of this section, we show that modularity constraints can be easily encoded using pseudo-Boolean axioms, and also that constraint sets consisting entirely of mod 2 constraints are easily solved either directly or using the above encoding, although it is not clear how to recover the pseudo-Boolean encodings from the Boolean versions.