Learning and inference

Before we present some experimental results related to the effectiveness of pseudo-Boolean inference, we should point out one additional problem that can arise in this setting. It is possible that for some branch variable $v$, the result of resolving the reasons for $v$ and $\neg v$ is a new nogood that is not falsified by the partial assignment above $v$ in the search space.

As an example [Dixon GinsbergDixon Ginsberg2002], suppose that we have a partial assignment $\{\neg a,\neg b,c,d\}$ and constraints

$$2e+a+c \geq 2$$ (31)

$$2\overline e+b+d \geq 2$$ (32)

Now we can unit propagate to conclude $e$ by virtue of (31) and $\neg e$ by virtue of (32); it isn't hard to conclude that the conflict set is $a\vee b$ in that either $a$ or $b$ must be true if (31) and (32) are to be simultaneously satisfiable. But if we simply add (31) and (32) and simplify, we get

$$a+b+c+d\geq 2$$

which still allows $a$ and $b$ to both be false. This difficulty can be addressed by deriving a cardinality constraint that is guaranteed to be falsified by the current partial solution being investigated [Dixon GinsbergDixon Ginsberg2002]; Chai and Kuehlmann Chai:pb have developed a still stronger method.