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:
In a similar way, we will say that the possible value of
under is given by
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
Conversely, suppose that
. Now the best we can do is
still to value the unvalued literals favorably, so that the value of
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.