TAOCP 7.2.2.2 Exercise 136

Section 7.2.2.2: Satisfiability

Exercise 136. [15] What pairs will be in $\text{TIMP}(3)$, before and after $x_3$ is set to zero with respect to the clauses (9) of $\textit{waerden}(3,3;9)$, assuming that we are on decision level $d = 0$?

Verified: no
Solve time: 2m22s

---

We restart from the formal definition used in TAOCP for TIMP.

A clause $(\ell_i \vee \ell_j \vee \ell_k)$ generates the three implications

$$ \bar{\ell}_i \wedge \bar{\ell}_j \to \ell_k,\quad \bar{\ell}_i \wedge \bar{\ell}_k \to \ell_j,\quad \bar{\ell}_j \wedge \bar{\ell}_k \to \ell_i. $$

The set $\text{TIMP}(3)$ consists of all such implication pairs arising from clauses that contain the variable $3$ or $\bar{3}$. No restriction is placed on whether $3$ appears in the antecedent or consequent of the implication.

1. Clauses of $\textit{waerden}(3,3;9)$ involving index $3$

The arithmetic progressions of length 3 in ${1,\dots,9}$ that contain $3$ are

$$ (1,2,3),\ (2,3,4),\ (3,4,5),\ (1,3,5),\ (3,5,7),\ (3,6,9). $$

Each progression contributes two clauses:

$$ (x_i \vee x_j \vee x_k), \qquad (\bar{x}_i \vee \bar{x}_j \vee \bar{x}_k). $$

Hence there are $12$ clauses in total, each producing $3$ implications, giving $36$ implication pairs in $\text{TIMP}(3)$ before any assignment.

2. Full implication set before setting $x_3 = 0$

We list all implications generated by each clause containing $3$. Each clause is expanded completely.

(1,2,3)

From $(x_1 \vee x_2 \vee x_3)$:

$$ \bar{1}\wedge \bar{2}\to 3,\quad \bar{1}\wedge \bar{3}\to 2,\quad \bar{2}\wedge \bar{3}\to 1. $$

From $(\bar{1} \vee \bar{2} \vee \bar{3})$:

$$ 1\wedge 2\to \bar{3},\quad 1\wedge 3\to \bar{2},\quad 2\wedge 3\to \bar{1}. $$

(2,3,4)

From $(x_2 \vee x_3 \vee x_4)$:

$$ \bar{2}\wedge \bar{3}\to 4,\quad \bar{2}\wedge \bar{4}\to 3,\quad \bar{3}\wedge \bar{4}\to 2. $$

From $(\bar{2} \vee \bar{3} \vee \bar{4})$:

$$ 2\wedge 3\to \bar{4},\quad 2\wedge 4\to \bar{3},\quad 3\wedge 4\to \bar{2}. $$

(3,4,5)

From $(x_3 \vee x_4 \vee x_5)$:

$$ \bar{3}\wedge \bar{4}\to 5,\quad \bar{3}\wedge \bar{5}\to 4,\quad \bar{4}\wedge \bar{5}\to 3. $$

From $(\bar{3} \vee \bar{4} \vee \bar{5})$:

$$ 3\wedge 4\to \bar{5},\quad 3\wedge 5\to \bar{4},\quad 4\wedge 5\to \bar{3}. $$

(1,3,5)

From $(x_1 \vee x_3 \vee x_5)$:

$$ \bar{1}\wedge \bar{3}\to 5,\quad \bar{1}\wedge \bar{5}\to 3,\quad \bar{3}\wedge \bar{5}\to 1. $$

From $(\bar{1} \vee \bar{3} \vee \bar{5})$:

$$ 1\wedge 3\to \bar{5},\quad 1\wedge 5\to \bar{3},\quad 3\wedge 5\to \bar{1}. $$

(3,5,7)

From $(x_3 \vee x_5 \vee x_7)$:

$$ \bar{3}\wedge \bar{5}\to 7,\quad \bar{3}\wedge \bar{7}\to 5,\quad \bar{5}\wedge \bar{7}\to 3. $$

From $(\bar{3} \vee \bar{5} \vee \bar{7})$:

$$ 3\wedge 5\to \bar{7},\quad 3\wedge 7\to \bar{5},\quad 5\wedge 7\to \bar{3}. $$

(3,6,9)

From $(x_3 \vee x_6 \vee x_9)$:

$$ \bar{3}\wedge \bar{6}\to 9,\quad \bar{3}\wedge \bar{9}\to 6,\quad \bar{6}\wedge \bar{9}\to 3. $$

From $(\bar{3} \vee \bar{6} \vee \bar{9})$:

$$ 3\wedge 6\to \bar{9},\quad 3\wedge 9\to \bar{6},\quad 6\wedge 9\to \bar{3}. $$

Summary before assignment

All $36$ implications above constitute $\text{TIMP}(3)$. The previous solution was incorrect because it omitted all implications where $3$ appears in the antecedent positions, even though they are part of the same clause-generated implication set.

3. After setting $x_3 = 0$

Setting $x_3 = 0$ makes $\bar{3}=1$. Therefore:

• Every clause containing $\bar{3}$ is satisfied and removed.
• Every clause containing $3$ reduces to a binary clause by deleting $3$.

After simplification, no clause in the resulting formula contains either $3$ or $\bar{3}$.

Indeed:

• Clauses of the form $(\bar{3} \vee \cdots)$ disappear.
• Clauses of the form $(x_3 \vee \ell_i \vee \ell_j)$ become $(\ell_i \vee \ell_j)$, which no longer mention variable $3$.

Hence the reduced formula contains no clauses involving variable $3$ at all.

4. $\text{TIMP}(3)$ after the assignment

Since $\text{TIMP}(3)$ is defined as the set of implications generated by clauses involving variable $3$, and no such clauses remain after setting $x_3 = 0$, we obtain

$$ \text{TIMP}(3) = \varnothing. $$

No binary implications survive in $\text{TIMP}(3)$ because all surviving binary clauses are over variables ${1,2,4,5,6,7,9}$ only.

Final answer

Before setting $x_3=0$, $\text{TIMP}(3)$ consists of all $36$ implication pairs listed above, generated from the 12 clauses containing index $3$.

After setting $x_3=0$, no clause contains variable $3$, hence

$$ \boxed{\text{TIMP}(3)=\varnothing.} $$