TAOCP 7.2.2.2 Exercise 267

Section 7.2.2.2: Satisfiability

Exercise 267. [25] Indexer-unit-SAT often contains numerous binary clauses, which are handled efficiently by the unit-propagation loop (62) of Algorithm I but not by the corresponding loop in step C3 of Algorithm C. (The technique of watched literals is great for long

clauses, but it is comparatively cumbersome for short ones.) What additional data structures will speed up Algorithm C's inner loop, when binary clauses are abundant?

Verified: no
Solve time: 4m22s

Solution

In Algorithm C, the inner loop of step C3 is designed around watched literals. For a clause $e$, the data structure records two watched literals $l_0$ and $l_1$, and propagation is triggered when one of these watched literals becomes false. The advantage of this method is that a long clause can usually be ignored after initialization, because only the watched literals need to be examined until one of them is falsified.

Binary clauses require a different treatment. If $e$ has the form ${l_0,l_1}$, then the falsification of one literal immediately forces the other literal. There is no unused literal that can replace a false watched literal, so the usual search performed in step C3 is unnecessary work. The binary case is therefore better handled by maintaining explicit implication information.

For every literal $l$, introduce a list $B_l$ of binary clauses containing $l$. If a binary clause is

${l,m},$

then add the implication

$\bar{l}\Rightarrow m$

to $B_{\bar{l}}$, and also add

$\bar{m}\Rightarrow l$

to $B_{\bar{m}}$.

During propagation, when Algorithm C assigns a literal $l$ to be true, it does not need to examine every watched binary clause containing $\bar{l}$. Instead, it scans the list $B_{\bar{l}}$. For every entry $\bar{l}\Rightarrow m$, the assignment $l=1$ makes the clause ${l,m}$ unit, so $m$ is forced. If $m$ is already false, a conflict is found immediately.

The existing watched-literal structures remain unchanged for clauses of length at least $3$. The new lists $B_l$ are used only for binary clauses, so step C3 can be modified by adding a binary-propagation pass before the ordinary watched-literal processing. Whenever a newly assigned literal $l$ is placed on the implication queue, the solver first processes all entries of $B_{\bar{l}}$, performing the same enqueue or conflict action that unit propagation would perform in Algorithm I. After this pass, the solver continues with the watched-literal loop for the longer clauses.

The reason this improves Algorithm C is that a binary clause never requires searching for a replacement watched literal. Its two possible watched literals are both the only literals in the clause, so the general watched-literal mechanism performs bookkeeping that cannot produce any benefit. The implication lists replace that bookkeeping by direct access to the only possible consequence of falsifying a literal.

The added storage is linear in the number of binary clauses. Each binary clause contributes exactly two directed implications, one for each possible falsification of one of its literals. Therefore, if there are $b$ binary clauses, the total size of the new data structures is $2b$ implication entries. The propagation work for a binary clause is reduced to a constant-time visit of the corresponding implication entry, rather than the watched-literal procedure of locating and testing another literal position.

Thus Algorithm C is augmented with implication lists $B_l$ for binary clauses, while its watched-literal data structures continue to handle longer clauses. This gives Algorithm C the same efficient treatment of binary clauses that Algorithm I obtains from its unit-propagation loop. $\boxed{\text{Add binary implication lists }B_l\text{ and process them during step C3.}}$