TAOCP 7.2.2.2 Exercise 25

Let $F$ be a 7SAT instance.

Section 7.2.2.2: Satisfiability

Exercise 25. [21] [21] Show that (18)–(19) and (20)–(21) are equally effective when $r = 2$.

Verified: no
Solve time: 5m55s


Setup

Let $F$ be a 7SAT instance. Let the variables of $F$ be chosen independently and uniformly from ${0,1}$.

For each clause $C$ of $F$, define the bad event $A_C$ to be the event that all literals of $C$ are false. Since $C$ has seven literals,

$$ \Pr(A_C)=2^{-7}. $$

We must prove that if every variable occurs in at most $13$ clauses, then there is an assignment avoiding every event $A_C$.

We use the variable form of the Lovász Local Lemma.

Variable Local Lemma. Suppose a family of bad events is determined by independent variables. If every bad event involves at most $k$ variables, every variable occurs in at most $D$ bad events, and

$$ D\le \frac{2^k}{k+1}, $$

then the probability that none of the bad events occurs is positive.

For this exercise we have $k=7$, and therefore it is enough to check

$$ 13\le \frac{2^7}{8}. $$

The right side is

$$ \frac{128}{8}=16, $$

so the hypothesis is satisfied.

Solution

Apply the lemma with the seven variables appearing in each clause as the independent variables determining the corresponding bad event.

A clause $C$ is false precisely when the seven variables of $C$ receive the unique assignment that falsifies each of its literals. Hence

$$ \Pr(A_C)=\frac1{2^7}. $$

Each event $A_C$ depends on at most seven independent variables. Each independent variable occurs in at most thirteen clauses, so the variable occurrence bound in the lemma is

$$ D=13. $$

The numerical condition required by the lemma becomes

$$ D\le \frac{2^7}{7+1}. $$

Substitution gives

$$ 13\le16, $$

which is true.

Therefore the family of bad events satisfies the hypotheses of the Local Lemma. Consequently,

$$ \Pr\left(\bigcap_C \overline{A_C}\right)>0 . $$

Hence there exists a truth assignment for which every clause avoids its corresponding bad event. Such an assignment satisfies every clause of $F$, so $F$ is satisfiable.

Therefore every 7SAT problem in which each variable occurs in at most $13$ clauses has a satisfying assignment.

This completes the proof. ∎

Verification

The only numerical inequality required is

$$ 13\le\frac{2^7}{8}. $$

Since

$$ 2^7=128, $$

we have

$$ \frac{2^7}{8}=16, $$

and the required bound is strict:

$$ 13<16. $$

The clause-failure probability is

$$ 2^{-7}=\frac1{128}, $$

because among the $2^7$ assignments to the seven variables of a clause, exactly one falsifies all seven literals. The dependence condition uses only the variables appearing in a clause, and each such variable participates in no more than thirteen bad events. The hypotheses of the Local Lemma are therefore satisfied.

The final conclusion is

$$ \boxed{\text{Every 7SAT formula with at most 13 occurrences of each variable is satisfiable.}} $$