TAOCP 7.2.2.2 Exercise 139

Let a binary clause $u \vee v$ be represented by the two implication edges u \to v, \qquad v \to u, and let $\mathrm{BIMP}(x)$ and $\mathrm{BPRED}(x)$ be maintained as mutual adjacency lists of succes...

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: 2m25s

Let a binary clause $u \vee v$ be represented by the two implication edges

$$ u \to v, \qquad v \to u, $$

and let $\mathrm{BIMP}(x)$ and $\mathrm{BPRED}(x)$ be maintained as mutual adjacency lists of successors and predecessors.

A newly inserted implication $v \to w$ must trigger the compensation rule: for every $u$ with $u \to v$, we must insert $u \to w$ if it is not already present.

1. Correct propagation mechanism

We maintain a queue $Q$ of newly created implication edges. Each element is a pair $(v,w)$ meaning that $w$ has just been inserted into $\mathrm{BIMP}(v)$ and has not yet been processed for propagation.

When processing $(v,w)$, we scan the current predecessor list $\mathrm{BPRED}(v)$. For each $u \in \mathrm{BPRED}(v)$, we test whether $w \in \mathrm{BIMP}(u)$. If not, we insert the edge $u \to w$, update both adjacency structures, and enqueue $(u,w)$.

This is exactly the transitive propagation of implication edges restricted to length-two inference steps:

$$ u \to v,\quad v \to w ;\Rightarrow; u \to w. $$

Correctness follows because every compensation resolvent corresponds to such a configuration at the moment $v \to w$ is processed, so every required edge is eventually generated, and no edge is generated unless justified by a valid resolvent.

2. Source of the efficiency issue

The flaw in the previous analysis is the assumption that each implication participates in only constant total work.

In fact, whenever a new edge $v \to w$ is inserted, the algorithm scans the entire set $\mathrm{BPRED}(v)$. If $v$ later acquires additional successors $w_1, w_2, \dots$, then $\mathrm{BPRED}(v)$ is scanned repeatedly, once per outgoing edge.

Thus a fixed pair $(u,v)$ can be examined multiple times, once for each newly created successor of $v$. The correct cost measure must account for repeated scans of the same predecessor list.

3. Correct efficiency analysis

Each time an implication $v \to w$ is inserted, the algorithm performs a scan of $\mathrm{BPRED}(v)$. Therefore the total work spent on scans is

$$ \sum_{(v,w)\ \text{inserted}} |\mathrm{BPRED}(v)|. $$

Equivalently, if we view the final implication graph, each successful insertion $v \to w$ contributes work proportional to the current in-degree of $v$ at that moment.

A more global bound is obtained by summing over all vertices:

$$ \sum_{v} \sum_{w:, v \to w \text{ is created}} |\mathrm{BPRED}(v)|. $$

This is naturally interpreted as being proportional to the number of length-two inference events

$$ (u,v,w) \quad \text{such that } u \to v \text{ exists when } v \to w \text{ is inserted}. $$

Each such triple causes exactly one membership test and at most one insertion attempt of $u \to w$. Hence:

  • Each successful implication $u \to w$ is created exactly once.
  • Each creation is charged to a unique triggering configuration $(u,v,w)$.
  • Each scan step is charged to the insertion of some edge $v \to w$.

Thus the total running time is

$$ O!\left(\sum_{v} \deg^{-}(v),\deg^{+}(v)\right) $$

evaluated over the evolving graph, or equivalently proportional to the number of realized compensation-resolvent checks.

4. What cannot be claimed

The previous claim that the running time is “linear in the size of the final implication closure” is not valid.

The final number of edges may be small while the number of intermediate two-step triggers can be much larger, since the same predecessor set $\mathrm{BPRED}(v)$ may be re-scanned many times as new outgoing edges of $v$ are discovered.

Therefore the correct efficiency statement is not linear in the final closure size, but proportional to the total number of compensation events, i.e., the number of triples $(u,v,w)$ examined during propagation.

5. Conclusion

The queue-based propagation algorithm is correct for maintaining closure under compensation resolvents.

Its correct efficiency characterization is:

$$ \text{time } = O(\text{number of generated edges } + \text{number of scanned pairs in BPRED lists}), $$

or more concretely,

$$ O!\left(\sum_{v} \deg^{-}(v),\deg^{+}(v)\right) $$

over the final implication structure.

This correctly accounts for repeated scans of predecessor lists and removes the unjustified linear-in-closure claim.