As with unit propagation, resolution also lifts fairly easily to a pseudo-Boolean setting. The general computation is as follows:
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:
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
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
One possibility is to rewrite (26) as a pair of cardinality