TAOCP 7.2.2.2 Exercise 139

Step L9 of Algorithm L is the point at which a newly discovered binary implication is inserted into the binary implication lists.

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 139. [25] (Compensation resolvents.) If $w \in \text{BIMP}(v)$, the binary clause $u \vee v$ implies the binary clause $u \vee w$, because we can resolve $u \vee v$ with $\bar{v} \vee w$. Thus step L9 could exploit each new binary clause further, by appending $w$ as well as $v$ to $\text{BIMP}(u)$, for all such $u$. Discuss how to do this efficiently.

Verified: yes
Solve time: 1m31s

Solution

Step L9 of Algorithm L is the point at which a newly discovered binary implication is inserted into the binary implication lists. Suppose that the clause $u\vee v$ is generated, and L9 records the implication

$\bar{u}\Rightarrow v.$

Equivalently, $v\in\operatorname{BIMP}(u)$. The ordinary action of L9 appends $v$ to $\operatorname{BIMP}(u)$ and $\bar{u}$ to $\operatorname{BIMP}(\bar{v})$, because every binary clause is represented by both of its directed implications.

The proposed compensation rule uses the transitive consequences of the new implication. If

$w\in\operatorname{BIMP}(v),$

then

$\bar{v}\vee w$

is present as a binary clause. Resolving

$u\vee v$

with

$\bar{v}\vee w$

on $v$ gives

$u\vee w.$

Therefore the new clause also implies

$w\in\operatorname{BIMP}(u).$

The direct implementation would examine every $u$ whose BIMP list contains $v$, and for every such $u$ scan the entire list $\operatorname{BIMP}(v)$, appending every $w$ found there. This approach repeats work because a variable may acquire many binary implications during the execution of Algorithm L.

A more efficient method is to regard every BIMP list as a set of arcs in the implication graph. A binary clause

$a\vee b$

is represented by the two implication arcs

$\bar{a}\rightarrow b,\qquad \bar{b}\rightarrow a.$

When L9 inserts a new arc

$\bar{u}\rightarrow v,$

the compensation resolvents are precisely the outgoing arcs from $v$. For each existing arc

$v\rightarrow w,$

we insert the composed arc

$\bar{u}\rightarrow w.$

The insertion can therefore be implemented as a graph-transitive update. The adjacency list of $v$ is scanned once, and the resulting targets are merged into the adjacency list of $\bar{u}$. Duplicate literals are ignored because $\operatorname{BIMP}(u)$ is a set of literals.

The same update must be performed for the opposite implication created by the binary clause. The insertion

$u\vee v$

also gives

$\bar{v}\rightarrow u.$

Hence every compensation resolvent generated from this side is obtained by scanning $\operatorname{BIMP}(u)$ and adding its elements to $\operatorname{BIMP}(\bar{v})$.

The important invariant is that every literal already placed in a BIMP list represents a valid binary implication. The direct insertion preserves this invariant because it inserts implications coming from existing binary clauses. The compensation insertion preserves it because each new implication

$\bar{u}\rightarrow w$

comes from the resolution of

$u\vee v$

with

$\bar{v}\vee w.$

Thus the added binary clause

$u\vee w$

is logically implied by clauses already present, and the invariant remains valid.

A practical implementation should not recursively follow newly created implications during the same update. Instead, it should maintain a queue of newly inserted implication arcs. When an arc $a\rightarrow b$ is removed from the queue, the current contents of $\operatorname{BIMP}(b)$ are scanned, and every missing arc $a\rightarrow c$ is inserted and placed on the queue. The queue terminates because there are only finitely many possible implication arcs, namely one for each ordered pair of distinct literals. Each arc is inserted at most once, so no resolvent is processed repeatedly.

The resulting version of L9 maintains the transitive closure of the binary implication relation reachable through binary clauses. The cost of later binary implication queries is reduced because every compensation resolvent that can be obtained by one more binary resolution step is already present in the corresponding BIMP list. The additional work is proportional to the number of newly inserted implication arcs and the total lengths of the BIMP lists that are scanned during those insertions.