Let us begin by discussing propagation techniques in a cardinality or
pseudo-Boolean setting.^{11}

A pseudo-Boolean version of unit propagation was first presented by Barth Barth:01 and is described in a number of papers [Aloul, Ramani, Markov, SakallahAloul et al.2002,Dixon GinsbergDixon Ginsberg2000]. In the Boolean case, we can describe a clause as unit if it contains no satisfied literals and at most one unvalued one. To generalize this to the pseudo-Boolean setting, we make the following definition, where we view a partial assignment simply as the set of literals that it values to true:

If no ambiguity is possible, we will write simply instead of . In other words, is the sum of the weights of literals that are already satisfied by , reduced by the required total weight .

In a similar way, we will say that the *possible value of
under * is given by

If no ambiguity is possible, we will write simply instead of . In other words, is the sum of the weights of literals that are either already satisfied or not valued by , reduced by the required total weight .

**Proof.** Assume first that
, and suppose that we value
every remaining variable in a way that helps to satisfy . Having
done so, every literal in that is not currently made false by
will be true, and the resulting value of will be

so that becomes satisfied.

Conversely, suppose that
. Now the best we can do is
still to value the unvalued literals favorably, so that the value of
becomes

and is unsatisfiable.

**Proof.** If there is a literal with weight
, setting
that literal to false will reduce
by , making it
negative and thus making the unsatisfiable. Conversely, if there
is no such literal, then
will remain positive after any
single unvalued literal is set, so that remains satisfiable and is
therefore not unit.

Given the above result, there is little impact on the time needed to find unit clauses. We need simply keep the literals in each clause sorted by weight and maintain, for each clause, the value of and the weight of the largest unvalued literal. If we value a literal with different weight, we can apply the test in Proposition 3.8 directly. If we value a literal of the given weight, a short walk along the clause will allow us to identify the new unvalued literal of maximum weight, so that the proposition continues to apply.