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 and , with given by
 (23)

and given by
 (24)

Then it is legitimate to conclude
 (25)

Proof. This is immediate. Multiply (23) by , multiply (24) by , add and simplify using .

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

Lemma 3.13   Suppose that is clause . Then is equivalent to , where the are given by:

Proof. If is a literal with , then both and the rewrite are true if is satisfied. If , then and the rewrite are equivalent.

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

as

because either is equivalent to .

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 and are disjoint. If there is a literal in that is the negation of a literal in , then we will have in (25), which we can simplify to 1 to make the resolved constraint trivial; resolution produces the same result. If there is a literal in that also appears in , the coefficient of that literal in the resolvent (25) will be 2 but can be reduced to 1 by virtue of the lemma.

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

 (26)

In other words, either is true or and 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

 (27) (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: Learning and Relevance Bounds Up: Pseudo-Boolean and Cardinality Constraints Previous: Watched literals
Matt Ginsberg 2004-02-19