TAOCP 7.2.2.2 Exercise 204
Working
Section 7.2.2.2: Satisfiability
Exercise 204. ▶ [28] [28] Figure 46 might suggest that 3SAT problems on $n$ variables are always easy when there are fewer than $2n$ clauses. We shall prove, however, that any set of $m$ ternary clauses on $n$ variables can be transformed mechanically into another set of ternary clauses on $N = O(m)$ variables in which no variable occurs more than four times. The transformed problem is satisfiable if and only if the original problem was; thus it isn't any simpler, although (with at most $4N$ literals) it has at most $\frac{4}{3}N$ clauses.
a) First replace the original $m$ clauses by $m$ new clauses $(X_1 \vee X_2 \vee X_2), \ldots, (X_{3m-2} \vee X_{3m-1} \vee X_{3m})$, on $3m$ new variables, and show how to add $3m$ clauses of size 2 so that the resulting $4m$ clauses have exactly as many solutions as the original. b) Construct 16 unsatisfiable ternary clauses on 15 variables, where each variable occurs at most 4 times. Hint: If $F$ and $F'$ are two sets of clauses, let $F \sqcup F'$ stand for any other set obtained from $F \cup F'$ by replacing one or more clauses $C$ of $F$ by $x \cup C$ and one or more clauses $C'$ of $F'$ by $\bar{x} \cup C'$, where $x$ is a new variable; then $F \sqcup F'$ is unsatisfiable whenever $F$ and $F'$ are both unsatisfiable. For example, if $F = {c}$ and $F' = {1, 1}$, then $F \sqcup F'$ is either ${2, 12, 12}$ or ${1, 2, 12}$ or ${2, 12, 1}$. c) Remove one of the clauses from solution (b) and find all solutions of the 15 clauses that remain (exactly three of the variables will have two solutions). d) Use (a), (b), and (c) to prove the $N$-variable result claimed above.
Verified: no
Solve time: 6m06s
Working