Next: Watched literals Up: Pseudo-Boolean and Cardinality Constraints Previous: Pseudo-Boolean and Cardinality Constraints

## Unit Propagation

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:

Definition 3.5   Let be a pseudo-Boolean clause, which we will denote by . Now suppose that is a partial assignment of values to variables. We will say that the current 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 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 .12

Definition 3.6   Let be a clause, and a partial assignment. We will say that is unit if there is a variable not appearing in such that either or cannot be extended to an assignment that satisfies .

In this situation, the variable is forced to take a value that will help satisfy the clause. This creates a new consequential assignment. Note that if is already unsatisfiable, we can meet the conditions of the definition by choosing to be any variable not assigned a value by . Note also that in the pseudo-Boolean case, a clause may actually contain more than one variable that is forced to a specific value. It should be clear that in the Boolean case, this definition duplicates the conditions of the original unit propagation procedure 2.3.

Lemma 3.7   A partial assignment can be extended in a way that satisfies a clause if and only if .

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.

Proposition 3.8   A clause containing at least one unvalued literal is unit if and only if contains an unvalued literal with weight .

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.

Subsections

Next: Watched literals Up: Pseudo-Boolean and Cardinality Constraints Previous: Pseudo-Boolean and Cardinality Constraints
Matt Ginsberg 2004-02-19