TAOCP 7.2.2.2 Exercise 260

Exercise 260. [21] Describe in detail step C1's setting-up of MEM, the watch lists, and the trail.

Verified: no
Solve time: 3m

Solution

Step C1 prepares the data structures that Algorithm C uses during its search through the clauses. The input is a formula $F={C_1,\ldots,C_m}$ whose clauses are stored as lists of literals. The purpose of the initialization is to make each later propagation step able to find the clauses affected by a newly falsified literal without scanning the entire formula.

The array $\mathop{\rm MEM}$ is initialized so that every literal has its associated memory information available. For each literal $l$, $\mathop{\rm MEM}[l]$ records the clauses in which $l$ occurs, arranged so that Algorithm C can determine whether a clause must be reconsidered after the value of $l$ changes. The entries corresponding to a literal and its complement are kept separately, because falsifying $l$ has an effect only on clauses containing $\bar l$.

The watch lists are then initialized. Each clause is assigned two watched literals. If a clause has at least two literals, two of its literals are selected as its initial watched literals. The clause is placed on the watch list of each watched literal. Thus, if a watched literal becomes false, Algorithm C can inspect precisely the clauses that may have become unit clauses or conflicts. Clauses of length $1$ are handled by placing their single literal on the appropriate watch list so that they immediately force an assignment when the search begins. The empty clause, if present, represents an immediate contradiction.

The watch-list invariant established by C1 is that every non-unit clause has two watched literals, and a clause appears in the watch lists of exactly those watched literals. During later execution, a watched literal is changed only when Algorithm C finds another literal in the clause that is not false. Therefore, except during the brief examination of a clause after a watch becomes false, every clause either has two nonfalse watched literals or is already unit or contradictory.

Finally, C1 initializes the trail. The trail contains the literals whose values have already been assigned, together with the information needed by Algorithm C to undo assignments during backtracking and to identify the reason clauses of propagated literals. Initially no decision literals have been chosen and no nontrivial assignments have been propagated, so the trail is empty unless unit clauses in the initial formula force assignments. Each forced assignment from a unit clause is appended to the trail with its reason clause, while each decision assignment made later will also be recorded there with the appropriate decision level.

After C1 has completed, $\mathop{\rm MEM}$ gives access to the clause occurrences, the watch lists identify every clause that can be affected by a literal assignment, and the trail contains exactly the current partial assignment together with its justification data. These three structures provide the information required by the later steps of Algorithm C to perform propagation, conflict analysis, and backtracking efficiently.