next up previous
Next: Inference and Resolution Up: Unit Propagation Previous: Unit Propagation

Watched literals

Generalizing the idea of watched literals is no more difficult. We make the following definition:

Definition 3.9   Let $c$ be a clause. A watching set for $c$ is any set $S$ of variables with the property that $c$ cannot be unit as long as all of the variables in $S$ are either unvalued or satisfied.

Proposition 3.10   Given a clause $c$ of the form $\sum_i w_i l_i \geq k$, let $S$ be any set of variables. Then $S$ is a watching set for $c$ if and only if
\begin{displaymath} \sum_i w_i - \max_i w_i \geq k \end{displaymath} (22)

where the sum and maximum are taken over literals involving variables in $S$.

Proof. Suppose that all of the variables in $S$ are unvalued or satisfied. Now let $l_j$ be any unvalued literal in $c$. If $l_j\not\in S$, then $\mbox{\tt poss}(c) \geq w_j + \sum_i w_i - k$ and thus $\mbox{\tt poss}(c) \geq w_j$ since $\sum_i w_i \geq \sum_i w_i - \max_i w_i \geq k$. If, on the other hand, $l_j\in S$, then

\begin{displaymath}\mbox{\tt poss}(c) \geq \sum_i w_i - k\end{displaymath}

and

\begin{displaymath}\sum_i w_i - w_j \geq \sum_i w_i - \max_i w_i \geq k\end{displaymath}

Combining these, we get

\begin{displaymath}\mbox{\tt poss}(c) \geq w_j\end{displaymath}

Either way, we cannot have $\mbox{\tt poss}(c) < w_j$ and Proposition 3.8 therefore implies that $c$ cannot be unit. It follows that $S$ is a watching set.

The converse is simpler. If $\sum_i w_i - \max_i w_i < k$, value every literal outside of $S$ so as to make $c$ false. Now $\mbox{\tt poss}(c) = \sum_i w_i - k$, so if $l_j$ is the literal in $S$ with greatest weight, the associated weight $w_j$ satisfies $w_j > \mbox{\tt poss}(c)$ and $c$ is unit. Thus $S$ cannot be a watching set.         $\mathchoice{\vcenter{\hrule height.4pt \hbox{\vrule width.4pt height3pt \kern ... ...vrule width.3pt height1.5pt \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$


This generalizes the definition from the Boolean case, a fact made even more obvious by:

Corollary 3.11   Given a cardinality constraint $c$ requiring at least $k$ of the associated literals to be true, $S$ is a watching set for $c$ if and only if it includes at least $k+1$ literals in $c$.

Proof. The expression (22) becomes

\begin{displaymath}\sum_i 1 - \max_i 1 \geq k\end{displaymath}

or

\begin{displaymath}\vert S\vert - 1 \geq k.\mbox{\nobreak\qquad$\mathchoice{\vce... ... \kern 1.5pt \vrule width.3pt} \hrule height.3pt}}$\medskip }\end{displaymath}

next up previous
Next: Inference and Resolution Up: Unit Propagation Previous: Unit Propagation
Matt Ginsberg 2004-02-19