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

$$\sum_i w_i l_i + wl \geq k$$ (23)

and $c'$ given by

$$\sum_i w'_i l'_i + w'\overline l \geq k'$$ (24)

Then it is legitimate to conclude

$$\sum_i w'w_i l_i + \sum_i ww'_i l'_i \geq w'k + wk' - ww'$$ (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:

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

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

$$3x+y+\overline z \geq 2$$

as

$$2x+y+\overline z \geq 2$$

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{array}{ccccccccc} a & + & b & + & c &&& \geq & 2 \\ a & + & & & \overline c & + & d & \geq & 1 \end{array}$$

which we add to get

$$2a + b + d \geq 2$$ (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

$$a+b \geq 1$$ (27)

$$a+d \geq 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.