TAOCP 7.2.2.2 Exercise 268

Section 7.2.2.2: Satisfiability

Exercise 268. [21] [21] When Algorithm C makes a literal false at level 0 of the trail, we can remove it from all of the clauses. Such updating might take a long time, if we did it "eagerly"; but there's a lazy way out: We can delete a permanently false literal if we happen to encounter it in step C3 while looking for a new literal to watch (see exercise 261).

Explain how to adapt the MEM data structure conventions so that such deletions can be done in situ, without copying clauses from one location into another.

Verified: no
Solve time: 3m10s

Solution

Algorithm C stores each clause $e$ in a MEM block whose entries can be accessed by links from the watched-literal data structures. The difficulty with deleting a literal from the middle of a clause is that moving the remaining literals would invalidate all references into the clause. The required modification is therefore to make the clause representation tolerate holes.

For each clause $e$, reserve a MEM block of fixed size equal to the original clause size, and keep the existing length field and watched-literal fields associated with the block. Introduce a distinguished empty entry, say $\bot$, which is not a literal and is never placed on a watch list. A deletion of a literal $l$ from $e$ changes only the entry containing $l$, replacing it by $\bot$. No other entry of the MEM block is moved.

During step C3, when Algorithm C scans the literals of a clause $e$ in order to find a new watched literal, the scan is modified as follows. A literal entry is treated in the usual way if it is a current literal. An entry equal to $\bot$ is skipped. If a literal $l$ is encountered that has become permanently false at level $0$, the entry containing $l$ is replaced by $\bot$, and the scan continues. Thus the deletion occurs at the same location in MEM where the obsolete literal was found.

The clause length field cannot count the number of occupied MEM entries after these deletions, because the block still contains deleted positions. Instead, maintain the number of live literals separately. If $e$ originally contained $k$ literals and $r$ of them have been deleted, the scan sees a block of $k$ positions containing exactly $k-r$ live literals and $r$ entries equal to $\bot$. The logical clause represented by the block is the set of its live literals.

The watch pointers remain valid because every pointer still refers to its original MEM position. When a watched literal is deleted, Algorithm C searches for a replacement among the remaining live entries. If a replacement is found, the corresponding watch pointer is changed in the same way as in the original algorithm. If no replacement exists, the clause has become unit or empty, and the ordinary unit-propagation or conflict handling of Algorithm C applies to the remaining live literals.

The same modification applies to all clause scans used by Algorithm C. Whenever a procedure follows a MEM link into a clause, it ignores $\bot$ entries and never follows a watch pointer to one. Consequently the data structures preserve the invariant that every watch pointer names a genuine literal position, while deleted literals disappear logically without requiring any physical relocation.

This representation has the required in situ property. A deletion changes one MEM entry and the live-literal count of the clause, but it does not copy the clause or alter the addresses of any surviving literals. Therefore all existing links into the clause remain correct.

This completes the proof. ∎