TAOCP 7.2.2.2 Exercise 233

Exercise 233. [16] Explain why (105) satisfies (104), by exhibiting $j(i)$ and $k(i)$ for $9 \le i \le 22$.

Verified: yes
Solve time: 2m55s

Solution

Let the clauses in the resolution chain (105) be denoted by $C_1,\ldots,C_{22}$ in the order in which they are displayed. The first eight clauses are the axioms, so equation (104) requires us only to specify $j(i)$ and $k(i)$ for $9\leq i\leq22$ such that

$C_i=C_{j(i)}\mathbin{\diamond}C_{k(i)},\qquad j(i)<i,\quad k(i)<i.$

The required choices are

$$ \begin{array}{c|c|c|c} i&C_i&j(i)&k(i)\ \hline 9&1\bar2\bar3&6&8\ 10&1\bar3&1&9\ 11&14&3&10\ 12&\bar3\bar4&7&10\ 13&24&4&11\ 14&2\bar4&2&12\ 15&2&13&14\ 16&\bar13&5&15\ 17&\bar34&6&13\ 18&1\bar4&8&14\ 19&\bar3&12&17\ 20&1&11&18\ 21&\bar1&16&19\ 22&\epsilon&20&21 \end{array} $$

Each entry satisfies (104) because the two preceding clauses contain complementary occurrences of one literal, and their resolvent is the stated clause. The derivations are as follows.

For $i=9$,

$C_6\diamond C_8=(\bar2\bar34)\diamond(\bar41\bar2)=1\bar2\bar3=C_9.$

For $i=10$,

$C_1\diamond C_9=(12\bar3)\diamond(1\bar2\bar3)=1\bar3=C_{10}.$

For $i=11$,

$C_3\diamond C_{10}=(341)\diamond(1\bar3)=14=C_{11}.$

For $i=12$,

$C_7\diamond C_{10}=(\bar3\bar4\bar1)\diamond(1\bar3)=\bar3\bar4=C_{12}.$

For $i=13$,

$C_4\diamond C_{11}=(4\bar12)\diamond(14)=24=C_{13}.$

For $i=14$,

$C_2\diamond C_{12}=(23\bar4)\diamond(\bar3\bar4)=2\bar4=C_{14}.$

For $i=15$,

$C_{13}\diamond C_{14}=(24)\diamond(2\bar4)=2=C_{15}.$

For $i=16$,

$C_5\diamond C_{15}=(\bar1\bar23)\diamond(2)=\bar13=C_{16}.$

For $i=17$, we may use $C_6$ and $C_{13}$:

$C_6\diamond C_{13}=(\bar2\bar34)\diamond(24)=\bar34=C_{17}.$

For $i=18$,

$C_8\diamond C_{14}=(\bar41\bar2)\diamond(2\bar4)=1\bar4=C_{18}.$

For $i=19$,

$C_{12}\diamond C_{17}=(\bar3\bar4)\diamond(\bar34)=\bar3=C_{19}.$

For $i=20$,

$C_{11}\diamond C_{18}=(14)\diamond(1\bar4)=1=C_{20}.$

For $i=21$,

$C_{16}\diamond C_{19}=(\bar13)\diamond(\bar3)=\bar1=C_{21}.$

Finally,

$C_{20}\diamond C_{21}=1\diamond\bar1=\epsilon=C_{22}.$

Thus every clause after the eight axioms is obtained from two earlier clauses by a valid resolution step, and the last clause is the empty clause. Therefore the sequence (105) satisfies the definition of a refutation chain given in (104).

This completes the proof. ∎