TAOCP 7.2.2.2 Exercise 30

Section 7.2.2.2: Satisfiability

Exercise 30. ▶ [22] [22] If auxiliary variables $s_j^i$ are used as in (18) and (19) to make $x_1 + \cdots + x_n \le r$, while $s_j^{i'}$ are used to make $\bar{x}_1 + \cdots + \bar{x}n \le n - r$, show that we may unify them by taking $s_j^{i'} = s{j-r}^{i'}$ for $1 \le j \le n - r$, $1 \le k \le r$. Can (20) and (21) be similarly unified?

Verified: no
Solve time: 2m40s

---

Solution

The two constraints

$$ x_1+\cdots+x_n\le r $$

and

$$ \bar{x}_1+\cdots+\bar{x}_n\le n-r $$

describe the same condition. The second inequality says that at most $n-r$ of the variables are false, which is equivalent to saying that at least $r$ of the variables are true. Together with the first inequality, this forces

$$ x_1+\cdots+x_n=r . $$

The auxiliary variables for the two sequential counters can therefore be identified by matching states that represent the same partial information.

For the first counter, $s_j^i$ represents the condition that among

$$ x_1,\ldots,x_i $$

there are at least $j$ true variables. The largest possible value of $j$ needed for the constraint $x_1+\cdots+x_n\le r$ is $r$. For the complementary counter, $s_j^{i'}$ represents the corresponding condition for

$$ \bar{x}_1,\ldots,\bar{x}_i . $$

Among the first $i$ variables, having at least $j$ false variables is equivalent to having at most $i-j$ true variables. In particular, when the two counters are combined into an equality counter, the complementary counter state indexed by $j$ corresponds to the original counter state indexed by $j-r$ after the shift by the required number $r$ of true variables.

Hence the auxiliary variables of the second counter may be renamed by

$$ s_j^{i'}=s_{j-r}^{i'} $$

for

$$ 1\le j\le n-r,\qquad 1\le i\le n . $$

The shift is valid because the second counter has indices

$$ 1\le j\le n-r, $$

so after shifting the index range becomes

$$ 1-r\le j-r\le n-2r . $$

The only indices that correspond to states required by the first counter are those obtained after the equality condition has removed the impossible lower states. These are exactly the shared states represented by the shifted variables. Thus no additional auxiliary variables are needed for the two upper-bound constraints.

For clauses (20) and (21), the same identification cannot be made in general. Clauses (18) and (19) describe the propagation of the sequential counter states, and the two copies have the same recursive structure after the index shift. Clauses (20) and (21) describe the strengthening clauses used to enforce the converse direction, and their literals occur with opposite polarities after replacing $x_i$ by $\bar{x}_i$. The shifted variables would therefore appear in clauses with incompatible roles unless additional transformations are made.

Consequently, the auxiliary variables of the two encodings of the upper bounds can be unified by the substitution

$$ \boxed{s_j^{i'}=s_{j-r}^{i'}}, $$

but the analogous unification of the clauses (20) and (21) is not possible without changing their form. This completes the proof. ∎