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

and given by

Then it is legitimate to conclude

**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
rewriting

as

because either is equivalent to .

**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

which we add to get

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

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.