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