TAOCP 7.2.2.2 Exercise 28

To require x_1+\cdots+x_n\ge 1, we can instead apply Sinz's construction for the equivalent condition

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 28. ▶ [20] [20] What clauses result from (18) and (19) when we want to ensure that $x_1 + \cdots + x_n \ge 1$? (This special case converts arbitrary clauses into 3SAT clauses.)

Verified: yes
Solve time: 2m03s

Solution

To require

$$ x_1+\cdots+x_n\ge 1, $$

we can instead apply Sinz's construction for the equivalent condition

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

In equations (18) and (19), set $r=n-1$ and replace each input variable $x_i$ by $\bar{x}_i$. The Sinz construction introduces variables

$$ s_j^k,\qquad 1\le j\le n-r,\quad 1\le k\le r . $$

Here

$$ n-r=n-(n-1)=1, $$

so the only possible value of $j$ is $j=1$. The variables are therefore

$$ s_1^1,s_1^2,\ldots,s_1^{n-1}. $$

The clauses in (18) have the form

$$ (\bar{s}j^k\vee s{j+1}^k), $$

but there are no such clauses because (18) requires $1\le j<n-r$, and here $n-r=1$.

The clauses in (19) become, after substituting $\bar{x}_i$ for $x_i$,

$$ (x_{j+k}\vee \bar{s}_j^k\vee s_j^{k+1}), $$

where the literal $\bar{s}_j^k$ is omitted when $k=0$ and $s_j^{k+1}$ is omitted when $k=r$. With $j=1$ and $r=n-1$, the cases are as follows.

For $k=0$ the clause is

$$ (x_1\vee s_1^1). $$

For

$$ 1\le k\le n-2, $$

the clauses are

$$ (x_{k+1}\vee \bar{s}_1^k\vee s_1^{k+1}). $$

For the final value $k=n-1$, the clause is

$$ (x_n\vee \bar{s}_1^{n-1}). $$

Thus the complete encoding of

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

obtained from Sinz's clauses is

$$ (x_1\vee s_1^1), $$

$$ (x_2\vee \bar{s}_1^1\vee s_1^2), $$

$$ (x_3\vee \bar{s}_1^2\vee s_1^3), $$

$$ \ldots, $$

$$ (x_{n-1}\vee \bar{s}_1^{n-2}\vee s_1^{n-1}), $$

$$ (x_n\vee \bar{s}_1^{n-1}). $$

The first and last clauses have length $2$, and the intermediate clauses have length $3$. The original constraint has therefore been replaced by clauses of length at most $3$, which is the desired conversion of an arbitrary clause into a 3SAT-compatible form.

This completes the proof. ∎