TAOCP 7.2.2.2 Exercise 26

Sinz's clauses are (\bar{s}_j^k\vee s_{j+1}^k), \qquad 1\le j<n-r,\quad 1\le k\le r, \tag{18}

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 26. [22] [22] Prove that Sinz's clauses (18) and (19) enforce the cardinality constraint $x_1 + \cdots + x_n \le r$. Hint: Show that they imply $s_j^i = 1$ whenever $x_1 + \cdots + x_{j+k-1} \ge k$.

Verified: yes
Solve time: 3m35s

Solution

Sinz's clauses are

$$ (\bar{s}j^k\vee s{j+1}^k), \qquad 1\le j<n-r,\quad 1\le k\le r, \tag{18} $$

and

$$ (\bar{x}_{j+k}\vee \bar{s}_j^k\vee s_j^{k+1}), \qquad 1\le j\le n-r,\quad 0\le k\le r, \tag{19} $$

where the literals $\bar{s}_j^0$ and $s_j^{r+1}$ are omitted. We prove that every satisfying assignment of these clauses has

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

The converse construction is not required, because the phrase "enforce the cardinality constraint" means that every satisfying assignment of the encoding must satisfy the intended constraint. The implication supplied by the hint is sufficient.

We first prove the property

$$ x_1+\cdots+x_{j+k-1}\ge k \quad\Longrightarrow\quad s_j^k=1 \tag{20} $$

for all $1\le k\le r$ and all $j$ for which $s_j^k$ occurs.

For $k=1$, suppose that

$$ x_1+\cdots+x_j\ge1 . $$

Choose an index $t\le j$ with $x_t=1$. Clause (19) with $k=0$ and index $j=t$ is

$$ (\bar{x}_t\vee s_t^1). $$

Since $x_t=1$, this clause forces

$$ s_t^1=1. $$

Clause (18) gives

$$ (\bar{s}u^1\vee s{u+1}^1) $$

for successive indices $u$. Hence

$$ s_t^1=1\Longrightarrow s_{t+1}^1=1 \Longrightarrow\cdots\Longrightarrow s_j^1=1 . $$

Therefore (20) holds for $k=1$.

Assume now that (20) holds for some $k<r$. Suppose that

$$ x_1+\cdots+x_{j+k}\ge k+1 . $$

Let $t$ be the position of the $(k+1)$st true variable among $x_1,\ldots,x_{j+k}$. The variables before $x_t$ contain at least $k$ true values, so

$$ x_1+\cdots+x_{t-1}\ge k . $$

The induction hypothesis gives

$$ s_{t-k}^k=1 . $$

Also,

$$ x_t=1 . $$

Clause (19) with index $j=t-k$ and value $k$ is

$$ (\bar{x}t\vee\bar{s}{t-k}^k\vee s_{t-k}^{k+1}). $$

The first two literals are false, so

$$ s_{t-k}^{k+1}=1 . $$

Using clause (18) repeatedly propagates this value:

$$ s_{t-k}^{k+1}=1 \Longrightarrow s_{t-k+1}^{k+1}=1 \Longrightarrow\cdots\Longrightarrow s_j^{k+1}=1 . $$

Thus (20) holds for $k+1$, completing the induction.

Now assume that the clauses are satisfied and suppose, for contradiction, that

$$ x_1+\cdots+x_n\ge r+1 . $$

Let $t$ be the position of the $(r+1)$st true variable. The first $t-1$ variables contain at least $r$ true values, so the property just proved gives

$$ s_{t-r}^r=1 . $$

Since $x_t=1$, clause (19) with $j=t-r$ and $k=r$ becomes

$$ (\bar{x}t\vee\bar{s}{t-r}^r), $$

because $s_{t-r}^{r+1}$ is omitted. Both literals in this clause are false, contradicting the assumption that all clauses are satisfied.

Therefore a satisfying assignment cannot have more than $r$ true variables, and hence

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

This completes the proof.

∎