TAOCP 7.2.2.2 Exercise 123
The previous construction used a one-watched-literal representation, but Algorithms B and D use the two-watched-literal representation.
Section 7.2.2.2: Satisfiability
Exercise 123. [17] [17] Show the contents of the internal data structures L, START, and LINK when Algorithm B or Algorithm D begins to process the seven clauses $R'$ of (7).
Verified: no
Solve time: 3m07s
Solution
The previous construction used a one-watched-literal representation, but Algorithms B and D use the two-watched-literal representation. The initialization therefore has to create watch lists containing two entries for every clause. The clauses are stored consecutively in $L$, and the first two literals of each clause are the initial watched literals, according to the initialization convention of the algorithm.
Write the clauses as
$$ R'={123,\ 2\bar3 4,\ 341,\ 4\bar1 2,\ \bar1 23,\ 234,\ \bar3 4\bar1}. $$
Each clause has length three, so the clause storage occupies $21$ literal positions. The clause starting positions are therefore
$$ \begin{array}{c|ccccccc} j&1&2&3&4&5&6&7\ \hline START(j)&1&4&7&10&13&16&19 \end{array} $$
and the literal array is
$$ \begin{array}{c|ccccccccccccccccccccc} p&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15&16&17&18&19&20&21\ \hline L(p)& 1&2&3& 2&\bar3&4& 3&4&1& 4&\bar1&2& \bar1&2&3& 2&3&4& \bar3&4&\bar1 \end{array} $$
so that
$$ \boxed{ L=(1,2,3,\ 2,\bar3,4,\ 3,4,1,\ 4,\bar1,2,\ \bar1,2,3,\ 2,3,4,\ \bar3,4,\bar1) } $$
and
$$ \boxed{ START=(1,4,7,10,13,16,19). } $$
It remains to construct the watch lists. The watched positions are the first two positions of every clause:
$$ \begin{array}{c|c|c} \text{clause}&\text{watched positions}&\text{watched literals}\ \hline 123&1,2&1,2\ 2\bar34&4,5&2,\bar3\ 341&7,8&3,4\ 4\bar12&10,11&4,\bar1\ \bar123&13,14&\bar1,2\ 234&16,17&2,3\ \bar34\bar1&19,20&\bar3,4 \end{array} $$
The link fields connect occurrences of the same watched literal. Using the usual initialization order, in which each new watched occurrence is inserted at the front of its literal's watch list, the watch lists are
$$ \begin{aligned} 1 &: 9\rightarrow1\rightarrow0,\ 2 &: 16\rightarrow14\rightarrow4\rightarrow2\rightarrow0,\ 3 &: 17\rightarrow15\rightarrow7\rightarrow3\rightarrow0,\ 4 &: 20\rightarrow18\rightarrow10\rightarrow8\rightarrow6\rightarrow0,\ \bar1 &: 13\rightarrow11\rightarrow0,\ \bar3 &: 19\rightarrow5\rightarrow0. \end{aligned} $$
Thus the head pointers for the six possible literals are
$$ \begin{array}{c|cccccc} l&1&2&3&4&\bar1&\bar3\ \hline LINK(l)&9&16&17&20&13&19 \end{array} $$
and the individual link fields at watched positions are
$$ \begin{array}{c|ccccccccccccccccccccc} p&1&2&3&4&5&6&7&8&9&10&11&12&13&14&15&16&17&18&19&20&21\ \hline LINK(p)& 0&0&0&0&0&0&3&6&1&8&0&0&11&4&7&14&15&10&5&18&0 \end{array} $$
where positions that are not watched have no link value.
Consequently the initial internal data structures are
$$ \boxed{ \begin{aligned} L={}&(1,2,3,\ 2,\bar3,4,\ 3,4,1,\ 4,\bar1,2,\ \bar1,2,3,\ 2,3,4,\ \bar3,4,\bar1),\[1mm] START={}&(1,4,7,10,13,16,19),\[1mm] LINK={}& (0,0,0,0,0,0,3,6,1,8,0,0,11,4,7,14,15,10,5,18,0), \end{aligned} } $$
together with the literal watch-list heads shown above.
Algorithm B and Algorithm D begin with the same clause storage and watch representation. Algorithm D differs only in the later search procedure, where it performs additional forced moves from unit clauses; this does not alter the initial $L$, $START$, and $LINK$ construction.