next up previous
Next: Learning and Relevance Bounds Up: Pseudo-Boolean and Cardinality Constraints Previous: Watched literals

Inference and Resolution

As with unit propagation, resolution also lifts fairly easily to a pseudo-Boolean setting. The general computation is as follows:

Proposition 3.12   Suppose that we have two clauses $c$ and $c'$, with $c$ given by
\begin{displaymath}
\sum_i w_i l_i + wl \geq k
\end{displaymath} (23)

and $c'$ given by
\begin{displaymath}
\sum_i w'_i l'_i + w'\overline l \geq k'
\end{displaymath} (24)

Then it is legitimate to conclude
\begin{displaymath}
\sum_i w'w_i l_i + \sum_i ww'_i l'_i \geq w'k + wk' - ww'
\end{displaymath} (25)

Proof. This is immediate. Multiply (23) by $w'$, multiply (24) by $w$, add and simplify using $l+\overline l=1$.         $\mathchoice{\vcenter{\hrule height.4pt
\hbox{\vrule width.4pt height3pt \kern ...
...vrule width.3pt height1.5pt \kern 1.5pt
\vrule width.3pt}
\hrule height.3pt}}$


If all of the weights, $k$ and $k'$ are 1, this generalizes conventional resolution provided that the sets of nonresolving literals in $c$ and $c'$ are disjoint. To deal with the case where there is overlap between the set of $l_i$ and the set of $l'_i$, we need:

Lemma 3.13   Suppose that $c$ is clause $\sum_i w_i l_i \geq k$. Then $c$ is equivalent to $\sum_i w'_i l_i \geq k$, where the $w'_i$ are given by:

\begin{displaymath}w'_i(j)=\cases{w_i,& if $w_i<k$;\cr
k,& otherwise.\cr}\end{displaymath}

Proof. If $l_j$ is a literal with $w_j\geq k$, then both $c$ and the rewrite are true if $l_j$ is satisfied. If $l_j = 0$, then $c$ and the rewrite are equivalent.         $\mathchoice{\vcenter{\hrule height.4pt
\hbox{\vrule width.4pt height3pt \kern ...
...vrule width.3pt height1.5pt \kern 1.5pt
\vrule width.3pt}
\hrule height.3pt}}$


In other words, we can reduce any coefficient that is greater than what is required to satisfy the clause in its entirety, for example rewriting

\begin{displaymath}3x+y+\overline z \geq 2\end{displaymath}

as

\begin{displaymath}2x+y+\overline z \geq 2\end{displaymath}

because either is equivalent to $x\vee(y\wedge \neg z)$.

Proposition 3.14   [Cook, Coullard, TuranCook et al.1987,HookerHooker1988] The construction of Proposition 3.12 generalizes conventional resolution.

Proof. We have already discussed the case where the sets of $l_i$ and $l'_i$ are disjoint. If there is a literal $l_i$ in $c$ that is the negation of a literal in $c'$, then we will have $l_i + \neg l_i$ in (25), which we can simplify to 1 to make the resolved constraint trivial; resolution produces the same result. If there is a literal $l_i$ in $c$ that also appears in $c'$, the coefficient of that literal in the resolvent (25) will be 2 but can be reduced to 1 by virtue of the lemma.         $\mathchoice{\vcenter{\hrule height.4pt
\hbox{\vrule width.4pt height3pt \kern ...
...vrule width.3pt height1.5pt \kern 1.5pt
\vrule width.3pt}
\hrule height.3pt}}$


Cardinality constraints are a bit more interesting. Suppose that we are resolving the two clauses

\begin{displaymath}\begin{array}{ccccccccc}
a & + & b & + & c &&& \geq & 2 \\
a & + & & & \overline c & + & d & \geq & 1
\end{array}\end{displaymath}

which we add to get
\begin{displaymath}
2a + b + d \geq 2
\end{displaymath} (26)

In other words, either $a$ is true or $b$ and $d$ both are. The problem is that this is not a cardinality constraint, and cannot be rewritten as one.

One possibility is to rewrite (26) as a pair of cardinality constraints

$\displaystyle a+b$ $\textstyle \geq$ $\displaystyle 1$ (27)
$\displaystyle a+d$ $\textstyle \geq$ $\displaystyle 1$ (28)

If, however, we want the result of ``resolving'' a pair of constraints to be a single axiom, we must either select one of the above axioms or extend our language further.


next up previous
Next: Learning and Relevance Bounds Up: Pseudo-Boolean and Cardinality Constraints Previous: Watched literals
Matt Ginsberg 2004-02-19