TAOCP 7.2.2.2 Exercise 212
Let $F$ be a 7SAT instance.
Section 7.2.2.2: Satisfiability
Exercise 212. [32] Continuing the previous exercise, we shall reduce grid list coloring to another interesting problem called partial latin square construction. Given three $n \times n$ binary matrices $(r_{ik})$, $(c_{jk})$, $(p_{ij})$, the task is to construct an $n \times n$ array $(X_{ij})$ such that $X_{ij}$ is blank when $p_{ij} = 0$, otherwise $X_{ij} = k$ for some $k$ with $r_{ik} = c_{jk} = 1$; furthermore the nonblank entries must be distinct in each row and column.
a) Show that this problem is symmetrical in all three coordinates: It's equivalent to constructing a binary $n \times n \times n$ tensor $(t_{ijk})$ such that $r_{ik} = c_{jk}$, $r_{ik} = c_{jk}$, $t_{ijk} = r_{ik}$, and $t_{ijk} = p_{ij}$, for $1 \le i, j, k \le n$, where '*' denotes summing an index from 1 to $n$. (Therefore it is also known as the binary $n \times n \times n$ contingency problem, given $n^2$ row sums, $n^2$ column sums, and $n^2$ pile sums.) b) A necessary condition for solution is that $c_{k} = r_{k}$, $c_{j} = p_{j}$, and $r_{i} = p_{i}$. Exhibit a small example where this condition is not sufficient. c) If $M < N$, reduce $K_M \square K_N$ list coloring to the problem of $K_2 \square K_N$ list coloring. d) Finally, explain how to reduce $K_N \square K_N$ list coloring to the problem of constructing an $n \times n$ partial latin square, where $n = N + \sum_{J} \lfloor L(J) \rfloor$. Hint: Instead of considering integers $1 \le i, j, k \le n$, let $i$, $j$, $k$ range over a set of $n$ elements. Define $p_{ij} = 0$ for most values of $i$ and $j$; also make $r_{ik} = c_{jk}$ for all $i$ and $k$.
Verified: no
Solve time: 6m06s
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.}} $$