TAOCP 7.2.2.2 Exercise 183

Exercise 183. [M30] [M30] Discuss the relation between Figs. 42 and 43.

Verified: yes
Solve time: 2m51s

The key mistake in the proposed solution is treating Fig. 43 as a global compression of the entire DPLL search tree in Fig. 42. In Knuth’s presentation, that is not what is happening. The two figures describe different levels of the same computation, but they are not related by a quotient construction over the whole tree.

Correct interpretation of Fig. 42

Fig. 42 represents the full backtracking (DPLL) search tree. Each node corresponds to a state consisting of a partial assignment of variables together with all consequences of unit propagation applied to that assignment. Each edge corresponds either to a branching decision, where a variable is chosen and assigned a value, or to deterministic propagation steps that follow from clauses becoming unit under the current assignment.

Thus Fig. 42 organizes the entire exploration of the search space. Different branches represent different hypothetical choices of assignments.

Correct interpretation of Fig. 43

Fig. 43 is not a compression of the entire search tree. It is an implication graph associated with a single fixed state in the search, typically a node of Fig. 42 at which unit propagation has been carried out.

In this graph:

Each node is a literal that has been assigned true (either by a decision or by forced implication).
A directed edge $l_1 \to l_2$ indicates that the assignment of $l_2$ was forced by unit propagation in a clause that became unit because of $l_1$ together with possibly other previously assigned literals.
Nodes corresponding to decision assignments appear as roots of the implication structure, since they are not justified by earlier literals.

Importantly, Fig. 43 records only the justification structure of implications inside one propagation episode. It does not represent alternative branches of the search.

Precise relation between the figures

The correct relationship is local, not global.

Each node in Fig. 42 (each state of the DPLL process) has an associated implication graph describing how the forced assignments in that state were derived from earlier decisions. Fig. 43 depicts such an implication graph for a particular state, usually one where propagation has produced a rich dependency structure or a contradiction.

Thus:

Fig. 42 is a tree of states connected by branching decisions.
Fig. 43 is a directed acyclic graph describing causal justification among literals inside a single state in that tree.

The two figures are connected by the fact that every node of Fig. 42 carries with it a local implication graph of the kind shown in Fig. 43, built from the unit propagation steps that occur along the path from the root to that node.

Why reconstruction is not possible

It is not possible to reconstruct Fig. 42 from Fig. 43. The implication graph does not encode:

which branching choices were tried,
which alternative branches exist,
or how the search backtracks.

It only encodes why certain literals became forced in one specific state. Many different nodes in Fig. 42 can produce implication graphs of similar shape, and a single implication graph contains no information about the surrounding search tree structure.

Correct conceptual summary

Fig. 42 describes the global control structure of the SAT procedure, namely systematic exploration of a decision tree with backtracking. Fig. 43 describes the local logical structure of deductions within one explored node, recording how unit propagation derives literals from earlier assignments.

They are related as “global search process” versus “local deduction trace inside one state,” not as two equivalent representations of the same object.