next up previous
Next: Summary Up: Proof Complexity Previous: Modularity constraints and pseudo-Boolean

Pseudo-Boolean constraints and extended resolution

Finally, let us clarify a point that we made earlier. Given that there is an encoding of $a\vee (b\wedge c)$ as a single pseudo-Boolean clause, how can it be that pseudo-Boolean inference is properly below extended resolution in the $p$-simulation hierarchy?

The answer is as follows. While the fact that $a\vee (b\wedge c)$ is logically equivalent to $2a+b+c\geq 2$ allows us to remove one of the variables introduced by extended resolution, we cannot combine this encoding with others to remove subsequent variables. As a specific example, suppose that we learn both

\begin{displaymath}a\vee (b\wedge c)\end{displaymath}


\begin{displaymath}d\vee (b\wedge c)\end{displaymath}

and wish to conclude from this that
(a\wedge d)\vee (b\wedge c)
\end{displaymath} (40)

There is no single pseudo-Boolean axiom that is equivalent to (40).

Matt Ginsberg 2004-02-19