TAOCP 7.2.2.2 Exercise 154

Start by restating the implication digraph and the subforest, then fix the level assignment so that every directed edge goes from a higher level to a lower level, as required.

taocpmathematicsalgorithmsvolume-4medium

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: 3m28s

Start by restating the implication digraph and the subforest, then fix the level assignment so that every directed edge goes from a higher level to a lower level, as required.

Implication digraph

From

$$ (a \lor b)\land(\bar a \lor \bar c)\land(c \lor d) $$

we obtain implications:

$$ \bar a \to b,\quad \bar b \to a,\quad a \to \bar c,\quad c \to \bar a,\quad \bar c \to d,\quad \bar d \to c. $$

1. Spanning subforest

We select the same subforest as before, which is valid since each vertex has at most one outgoing edge and all literals are included:

$$ \bar d \to c \to \bar a \to b, \qquad \bar b \to a \to \bar c \to d. $$

This is a directed spanning forest on the eight literals with two trees rooted at $\bar d$ and $\bar b$. It is acyclic by construction.

2. Correct truth-level assignment

The error in the previous solution was the direction of the level ordering. Since edges must go from higher level to lower level, the roots must be placed at the highest level.

Assign levels as follows:

  • Level 3 (roots):

$$ \bar d,\ \bar b $$

  • Level 2:

$$ c,\ a $$

  • Level 1:

$$ \bar a,\ \bar c $$

  • Level 0:

$$ b,\ d $$

Thus the ordering is:

$$ \bar d,\ \bar b;\ c,\ a;\ \bar a,\ \bar c;\ b,\ d. $$

3. Verification of edge direction

Check each edge of the subforest:

  • $\bar d(3) \to c(2)$
  • $c(2) \to \bar a(1)$
  • $\bar a(1) \to b(0)$
  • $\bar b(3) \to a(2)$
  • $a(2) \to \bar c(1)$
  • $\bar c(1) \to d(0)$

Every edge goes from a higher level to a lower level, as required.

Conclusion

The subforest is correct, and with the corrected level assignment it satisfies the required monotonicity condition for lookahead propagation analogous to (70).