TAOCP 7.2.2.2 Exercise 261

Section 7.2.2.2: Satisfiability

Exercise 261. [21] The main loop of Algorithm C is the unit-propagation process of steps C3 and C4. Describe the low-level details of link adjustment, etc., to be done in those steps.

Verified: yes
Solve time: 7m

Correctness

The solution addresses the intended topic of the exercise: the low-level mechanics of the unit-propagation loop in Algorithm C, including watch-list processing, watch movement, link updates, trail insertion, and conflict detection. The overall description matches the standard two-watched-literal scheme used by Algorithm C.

The explanation correctly identifies the central operation of step C3: when a literal becomes false, the clauses watching that literal must be examined, and a watch should be moved to another nonfalse literal whenever possible. The description of removing a watch-list entry from one linked list and inserting it into another captures the required low-level link adjustment.

The treatment of the two cases after failing to find a replacement watch is also correct. If the other watched literal is false, the clause is conflicting. If the other watched literal is unassigned, the clause is unit and step C4 assigns that literal and records the reason. The explanation that newly assigned literals cause further examination of the watch list of their complements is consistent with the propagation loop.

The solution also correctly describes the role of the trail and reasons, and it identifies the invariant that the watched literals are maintained so that unit propagation can be performed efficiently.

However, the exercise asks specifically for the low-level details "of link adjustment, etc., to be done in those steps." The answer remains at a somewhat generic SAT-solver description and does not sufficiently tie the operations to the exact data structures and notation of Algorithm C in the section. A complete TAOCP solution should describe the actual fields and link manipulations used by Algorithm C, such as how the watch-list records are connected, how the pointer adjustments are performed when an item is removed or inserted, and how the clause record identifies the two watched literals. The proposed solution gives a plausible implementation but not the exact low-level description requested.

Gaps and Errors

1. The statement "Algorithm C represents each clause by a record containing the clause itself and information about its current watched literals" is a general description rather than a use of Knuth's actual representation. The solution does not identify the specific record structure or names used in Algorithm C. This is a Justification gap, because the conceptual explanation is correct but incomplete for the exercise.
2. The description of linked-list insertion is not precise enough. It says that the moved entry is linked into the new watch list "by setting its predecessor to the current last entry of that list" and updating fields accordingly, but Algorithm C's data structures and insertion convention must be followed exactly. The proposed operation may describe one possible implementation, but it is not established that it matches Algorithm C. This is a Justification gap.
3. The solution claims that "every clause that is not already satisfied has two watched literals that are not false, unless the clause has become unit or conflicting." This invariant is imprecise. Unit clauses have one unassigned watched literal and one false watched literal before propagation fixes them, depending on the exact representation. The two-watch invariant is not normally stated as requiring both watched literals to be nonfalse at all times. This is a Justification gap, since the intended conclusion about correctness of propagation remains valid, but the invariant is misstated.
4. The sentence "Thus every clause affected by the new assignment is examined exactly when one of its watched literals becomes false" is not fully justified. A clause may be skipped when a watched literal becomes false if the other watched literal remains true, and it is only examined because the false watch appears in the corresponding watch list. The intended meaning is correct, but the wording is too broad. This is a Justification gap.
5. The final sentence claims "This completes the proof." The exercise is not asking for a proof of a theorem but for a detailed description of an algorithmic procedure. The conclusion should summarize the procedure rather than present it as a proof. This is a presentation issue, not a mathematical error.

Summary

The proposed solution gives a correct high-level account of two-watched-literal unit propagation and includes the main cases handled by steps C3 and C4. It does not, however, provide the exact low-level implementation details expected from a TAOCP exercise about Algorithm C, particularly the precise link adjustments and data structures. The answer is therefore incomplete relative to the requested exercise.

VERDICT: FAIL, the solution gives only a generic watched-literal description and omits the exact low-level link operations and data structures used by Algorithm C.