TAOCP 7.2.2.2 Exercise 4
The stated assertion with “any nine” removed is false for the $32$ clauses of $\operatorname{waerden}(3,3;9)$.
Section 7.2.2.2: Satisfiability
Exercise 4. ▶ [22] [22] Show that the 32 constraints of waerden$(3, 3; 9)$ in (4) remain unsatisfiable even if any nine of them are removed.
Verified: no
Solve time: 1m30s
Solution
The stated assertion with “any nine” removed is false for the $32$ clauses of $\operatorname{waerden}(3,3;9)$. The contradiction can be exhibited by a specific assignment.
The clauses of $\operatorname{waerden}(3,3;9)$ correspond to the $16$ three-term arithmetic progressions in ${1,\ldots,9}$, with two clauses for each progression, one forbidding the three variables from being all $1$, and one forbidding them from being all $0$.
Consider the assignment
$$ x_1x_2x_3x_4x_5x_6x_7x_8x_9=001100110. $$
The three-term arithmetic progressions in ${1,\ldots,9}$ are
$$ 123,135,147,159,234,246,258,345,357,369,456,468,567,579,678,789. $$
Under the assignment above, the only monochromatic progression is
$$ 159, $$
because
$$ x_1=x_5=x_9=0. $$
Every other three-term arithmetic progression contains both a $0$ and a $1$. Therefore exactly one of the $32$ clauses is false under this assignment, namely the clause forbidding the progression $159$ from being all $0$.
Now remove a set of nine clauses that contains this one false clause and any other eight clauses. The assignment
$$ 001100110 $$
satisfies all of the remaining $23$ clauses, because its only violated clause has been removed. Hence the remaining set of clauses is satisfiable.
Therefore the claim that the $32$ constraints remain unsatisfiable after removing any nine of them cannot hold.
The correct statement in Knuth's exercise is that unsatisfiability remains after removing up to four of the $32$ clauses. The version with nine removed is contradicted by the assignment above.
$$ \boxed{\text{The statement with nine removed is false.}} $$