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: yes
Solve time: 2m04s

---

Solution

A ternary clause $l_1l_2l_3$ contributes three entries to the TIMP structure. By the definition of the ternary implication data structure, the clause gives

$$ \bar{l}_1\to l_2\vee l_3,\qquad \bar{l}_2\to l_1\vee l_3,\qquad \bar{l}_3\to l_1\vee l_2 . $$

Hence $\operatorname{TIMP}(3)$ contains the pairs $(u,v)$ for which a clause of the form

$$ \bar{3}uv $$

occurs among the ternary clauses of $\mathit{waerden}(3,3;9)$.

The clauses (9) are obtained from the arithmetic progressions of length three in ${1,\ldots,9}$. The progressions containing $3$ are

$$ 123,\quad 234,\quad 345,\quad 135,\quad 357,\quad 369 . $$

For each progression, the clause forbidding three $1$'s is the clause containing the complemented literals. These are precisely the clauses containing $\bar{3}$:

$$ \bar1\bar2\bar3,\quad \bar2\bar3\bar4,\quad \bar3\bar4\bar5,\quad \bar1\bar3\bar5,\quad \bar3\bar5\bar7,\quad \bar3\bar6\bar9 . $$

Applying the TIMP rule to each clause gives respectively the pairs

$$ (\bar1,\bar2),\quad (\bar2,\bar4),\quad (\bar4,\bar5),\quad (\bar1,\bar5),\quad (\bar5,\bar7),\quad (\bar6,\bar9). $$

Therefore, before $x_3$ is assigned,

$$ \operatorname{TIMP}(3)

{(\bar1,\bar2),(\bar2,\bar4),(\bar4,\bar5), (\bar1,\bar5),(\bar5,\bar7),(\bar6,\bar9)}. $$

Now set $x_3$ to zero. The true literal is then $\bar3$. Every ternary clause containing $\bar3$ becomes satisfied and is removed from the active TIMP lists. The six clauses listed above are exactly the clauses that supplied the six entries of $\operatorname{TIMP}(3)$, so none of those pairs remains active.

No other ternary clause can contribute an entry to $\operatorname{TIMP}(3)$, because such an entry would require the clause to contain $\bar3$, and all such clauses have already been satisfied.

Thus after $x_3$ is set to zero at decision level $d=0$,

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

The requested values are therefore

$$ \boxed{\operatorname{TIMP}(3)\text{ before }x_3=0

{(\bar1,\bar2),(\bar2,\bar4),(\bar4,\bar5), (\bar1,\bar5),(\bar5,\bar7),(\bar6,\bar9)}} $$

and

$$ \boxed{\operatorname{TIMP}(3)\text{ after }x_3=0

\varnothing } . $$