Next: Inference and Resolution
Up: Unit Propagation
Previous: Unit Propagation
Generalizing the idea of watched literals
is no more difficult. We make the following definition:
Definition 3.9
Let
![$c$](img26.png)
be a clause. A
watching set for ![$c$](img26.png)
is any set
![$S$](img140.png)
of variables with the property that
![$c$](img26.png)
cannot be unit
as long as all of the variables in
![$S$](img140.png)
are either unvalued or
satisfied.
Proposition 3.10
Given a clause
![$c$](img26.png)
of the form
![$\sum_i w_i l_i \geq k$](img146.png)
,
let
![$S$](img140.png)
be any set of variables. Then
![$S$](img140.png)
is a watching set for
![$c$](img26.png)
if and only if
![\begin{displaymath}
\sum_i w_i - \max_i w_i \geq k
\end{displaymath}](img161.png) |
(22) |
where the sum and maximum are taken over literals involving variables in
![$S$](img140.png)
.
Proof. Suppose that all of the variables in
are unvalued or
satisfied. Now let
be any unvalued literal in
. If
, then
and thus
since
. If, on the other hand,
, then
and
Combining these, we get
Either way, we cannot have
and Proposition 3.8 therefore
implies that
cannot be unit. It follows that
is a watching set.
The converse is simpler. If
, value
every literal outside of
so as to make
false. Now
, so if
is the literal in
with greatest
weight, the associated weight
satisfies
and
is unit. Thus
cannot be a watching set.
This generalizes the definition from the Boolean case, a fact made
even more obvious by:
Corollary 3.11
Given a cardinality constraint
![$c$](img26.png)
requiring at
least
![$k$](img9.png)
of the associated literals to be true,
![$S$](img140.png)
is a watching set
for
![$c$](img26.png)
if and only if it includes at least
![$k+1$](img176.png)
literals in
![$c$](img26.png)
.
Proof. The expression (22) becomes
or
Next: Inference and Resolution
Up: Unit Propagation
Previous: Unit Propagation
Matt Ginsberg
2004-02-19