TAOCP 7.2.2.2 Exercise 382
Let C_i=(\bar{x}_i\vee x_{i+1}) for $1\le i<n$, and let
Section 7.2.2.2: Satisfiability
Exercise 382. [30] [30] Although the techniques in the preceding exercises are computationally difficult to apply, show that a lookahead forest based on the dependency digraph can be used to discover some of those simplifications efficiently.
Verified: no
Solve time: 5m55s
Solution
Let
$$ C_i=(\bar{x}i\vee x{i+1}) $$
for $1\le i<n$, and let
$$ C_n=(\bar{x}_n\vee x_1). $$
The formula in the exercise is
$$ C_1\wedge C_2\wedge\cdots\wedge C_n . $$
Suppose that no other clauses contain negative literals. We prove that any one of these clauses may be removed without changing satisfiability. By symmetry it is sufficient to remove $C_n$.
After removing $C_n$, the remaining clauses are
$$ (\bar{x}_1\vee x_2)\wedge(\bar{x}2\vee x_3)\wedge\cdots\wedge(\bar{x}{n-1}\vee x_n). $$
We first show that this weakened formula implies the removed clause. If all clauses $C_1,\ldots,C_{n-1}$ hold, then
$$ x_1\Rightarrow x_2\Rightarrow\cdots\Rightarrow x_n . $$
Hence if $x_n=0$, then successively
$$ x_{n-1}=0,\quad x_{n-2}=0,\quad\ldots,\quad x_1=0 . $$
Therefore the only possible violation of
$$ \bar{x}_n\vee x_1 $$
would be an assignment with
$$ x_n=1,\qquad x_1=0 . $$
The remaining clauses rule this out, because $x_1=0$ forces $x_2=0$, then $x_3=0$, and so on, finally forcing $x_n=0$. Thus every satisfying assignment of the formula with $C_n$ removed already satisfies $C_n$.
Consequently removing $C_n$ preserves satisfiability. Since the clauses are invariant under the cyclic permutation
$$ x_1\mapsto x_2\mapsto\cdots\mapsto x_n\mapsto x_1, $$
the same argument applies to every $C_i$. Hence any one clause in the displayed conjunction can be removed.
The connection with exercises 379 and 380 is as follows. Exercise 379 permits a clause containing a literal $a$ to be shortened when every potentially dangerous clause containing $\bar a$ is blocked by another literal. In the present formula, the only clauses containing negative literals are the chain clauses themselves, so the shortening condition is satisfied at each stage. Applying blocked self-subsumption repeatedly shortens a chosen clause until the remaining weakened clause is implied by the others. Exercise 380 then permits the resulting weak clause to be eliminated.
For example, after removing $C_n$, the remaining clauses imply the shortened form obtained from $C_n$, because the chain
$$ x_1\Rightarrow x_2\Rightarrow\cdots\Rightarrow x_n $$
already enforces the missing implication. Thus the original clause is redundant.
No erp rule is needed for this deletion. The only operations used are the satisfiability-preserving shortenings from exercise 379 and the eliminations justified in exercise 380. Neither operation requires the introduction of new variables or any additional equivalence-preserving replacement.
The required erp rules are therefore none: the transformation is obtained entirely by the blocked self-subsumption and clause-elimination rules already established in exercises 379 and 380.
This completes the proof.
∎