TAOCP 7.2.2.2 Exercise 154
The three clauses give the implication digraph obtained from the usual binary-clause rule.
Section 7.2.2.2: Satisfiability
Exercise 154. [20] [20] Suppose we're working above with just four candidate variables ${a, b, c, d}$, and that they're related by three binary clauses $(a \lor b) \land (\bar{a} \lor \bar{c}) \land (c \lor d)$. Find a subforest and a sequence of truth levels to facilitate lookaheads, analogous to (69) and (70).
Verified: yes
Solve time: 1m47s
Solution
The three clauses give the implication digraph obtained from the usual binary-clause rule. The clause $(u\lor v)$ gives the two implications $\bar{u}\to v$ and $\bar{v}\to u$. Hence the clauses
$$ (a\lor b),\qquad (\bar a\lor \bar c),\qquad (c\lor d) $$
give the arcs
$$ \bar a\to b,\qquad \bar b\to a, $$
$$ a\to \bar c,\qquad c\to \bar a, $$
$$ \bar c\to d,\qquad \bar d\to c . $$
A suitable subforest is obtained by taking the two directed trees
$$ \bar b\to a\to \bar c\to d $$
and
$$ \bar d\to c\to \bar a\to b . $$
Each literal occurs exactly once in this forest, and every selected arc is an arc of the implication digraph. The omitted arcs are
$$ \bar a\to b,\qquad \bar c\to d $$
only if they duplicate the selected parent-child relations; no additional information is needed from them for the lookahead levels.
To assign truth levels in the sense of (70), list each descendant before its predecessor and assign larger offsets to literals that are farther from the roots. One possible ordering is
$$ d,\ \bar c,\ a,\ \bar b,\ b,\ \bar a,\ c,\ \bar d , $$
with offsets
$$ o(d)=3,\quad o(\bar c)=2,\quad o(a)=1,\quad o(\bar b)=0, $$
and
$$ o(b)=3,\quad o(\bar a)=2,\quad o(c)=1,\quad o(\bar d)=0 . $$
For every forest arc $v\to u$, the literal $u$ occurs before $v$ in the ordering and has a larger offset. Thus the dependency information is captured by the levels: setting a literal at one level forces the literals below it in the corresponding tree. The two roots $\bar b$ and $\bar d$ represent the two independent starting points of the lookahead structure.
Therefore a valid subforest and associated truth levels are
$$ \boxed{ \bar b\to a\to\bar c\to d,\qquad \bar d\to c\to\bar a\to b } $$
with the offsets given above. This completes the proof.
∎