next up previous
Next: Modularity constraints and pseudo-Boolean Up: Pseudo-Boolean and Cardinality Constraints Previous: Experimental results

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
\begin{displaymath}
\sum_i w_i l_i~\equiv n (\mbox{\rm mod}\ m)
\end{displaymath} (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.



Subsections
next up previous
Next: Modularity constraints and pseudo-Boolean Up: Pseudo-Boolean and Cardinality Constraints Previous: Experimental results
Matt Ginsberg 2004-02-19