TAOCP 7.2.2.2 Exercise 209
The reviewer feedback identifies a mismatch between the stated hypothesis and the hypothesis of the actual TAOCP exercise.
Section 7.2.2.2: Satisfiability
Exercise 209. [25] [25] (C. A. Tovey.) Prove that every $k$SAT formula in which each literal occurs more than $k$ times is satisfiable. (Thus the limits on occurrences in exercises 204–208 cannot be lowered, when $k = 3$ and $k = 4$.) Hint: Use the theory of bipartite matching.
Verified: no
Solve time: 4m41s
The reviewer feedback identifies a mismatch between the stated hypothesis and the hypothesis of the actual TAOCP exercise. Exercise 7.2.2.2.209 states that no variable occurs more than $k$ times, not that every literal occurs more than $k$ times. Under the literal-occurrence hypothesis given in the prompt, the proposed matching proof does not apply. The following is the corrected solution to the TAOCP exercise.
Solution
Let the $k$-SAT formula have clauses
$$ C_1,C_2,\ldots,C_m . $$
Assume that every variable occurs in at most $k$ clauses, counting both its positive and negative occurrences. We construct a bipartite graph $G=(A,B,E)$.
The left part $A$ consists of the clauses $C_1,\ldots,C_m$. The right part $B$ consists of the variables of the formula. There is an edge between $C_i$ and $x$ exactly when either $x$ or $\bar{x}$ occurs in $C_i$.
We prove that every clause can be matched with a distinct variable. By Hall's theorem, it is enough to prove that for every set $S$ of clauses,
$$ |N(S)|\geq |S|, $$
where $N(S)$ is the set of variables appearing in the clauses of $S$.
Take any subset $S$ of clauses. Each clause contains exactly $k$ literals, so the clauses in $S$ contain altogether
$$ k|S| $$
literal occurrences.
Every variable appearing in these clauses belongs to $N(S)$. By hypothesis, each variable occurs at most $k$ times in the whole formula, and therefore it can account for at most $k$ of the literal occurrences appearing among the clauses of $S$. Hence all variables in $N(S)$ together can account for at most
$$ k|N(S)| $$
occurrences.
The $k|S|$ occurrences contributed by the clauses in $S$ must therefore satisfy
$$ k|S|\leq k|N(S)|. $$
Since $k>0$, division by $k$ gives
$$ |S|\leq |N(S)|. $$
Thus Hall's condition holds. Therefore there exists a matching that covers every clause. Let the matching assign clause $C_i$ a distinct variable $x_i$ that occurs in $C_i$.
Now define a truth assignment. For every matched pair $(C_i,x_i)$, set $x_i$ so that the particular literal involving $x_i$ in $C_i$ becomes true. This choice is always possible because each variable is matched to at most one clause, so no variable is required to satisfy two different clauses with opposite values.
Variables that are not matched may be assigned arbitrary values.
Every clause $C_i$ contains its matched literal, and that literal has been made true. Hence every clause is satisfied. Therefore the entire $k$-SAT formula is satisfiable.
$$ \boxed{\text{Every (k)-SAT formula in which no variable occurs more than (k) times is satisfiable.}} $$
The matching argument therefore proves the theorem stated in TAOCP Exercise 7.2.2.2.209. The version with the condition that every literal occurs more than $k$ times is a different statement and is not what the given bipartite matching hint addresses.