Strengthening

The specific method that we will discuss is from operations research and is used to preprocess mixed integer programming problems [Guignard SpielbergGuignard Spielberg1981,SavelsberghSavelsbergh1994].

Suppose that after setting $l_0$ to true and applying some form of propagation to our constraint set, we discover that under this assumption a constraint $c$ given by $\sum w_i l_i \geq r$ becomes oversatisfied by an amount $s$ in that the sum of the left hand side is greater (by $s$) than the amount required by the right hand side of the inequality; in the terms of Definition 3.5, $\mbox{\tt curr}(c) = s$. The oversatisfied constraint $c$ can now be replaced by the following:

$$s\overline l_0 + \sum w_i l_i \geq r + s$$ (29)

If $l_0$ is true, we know that $\sum w_i l_i \geq r + s$, so (29) holds. If $l_0$ is false, then $s\overline l_0 = s$ and we still must satisfy the original constraint $\sum w_i l_i \geq r$, so (29) still holds. The new constraint implies the original one, so no information is lost in the replacement.

As we have remarked, the OR community uses this technique during preprocessing. A literal is fixed, propagation is applied, and any oversatisfied constraint is strengthened. Consider the following set of clauses:

$$\begin{eqnarray*} & a + b \geq 1 & \\ & a + c \geq 1 & \\ & b + c \geq 1 & \end{eqnarray*}$$

If we set $a$ to false, we must then value both $b$ and $c$ true in order to satisfy the first two constraints. The third constraint is now oversatisfied and can thus be replaced by

$$a + b + c \geq 2$$

The power of this method is that it allows us to build more complex axioms from a set of simple ones. The strengthened constraint will often subsume some or all of the constraints involved in generating it. In this case, the new constraint subsumes all three of the generating constraints.

Proposition 3.17   Let $c$ be a constraint and $P$ a partial assignment. Then if we can conclude that $\mbox{\tt curr}(c)\geq s$ for any solution to our overall problem that extends $P$, we can replace $c$ with

$$s \sum_P \overline l_i + \sum w_i l_i \geq r + s$$ (30)

where the first summation is over literals $l_i\in P$.

Proof. For any truth assignment that extends $P$, (30) follows from the fact that $\mbox{\tt curr}(c)\geq s$. For any truth assignment $P'$ that does not extend $P$, there is some $l_j\in P$ that is false in $P'$, and so

$$s \sum_P \overline l_i \geq s$$

Combining this with the original constraint $c$ once again produces (30).         $\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}}$