TAOCP 7.2.2.2 Exercise 135

Section 7.2.2.2: Satisfiability

Exercise 135. ▶ [16] The literals $l'$ in $\text{BIMP}(l)$ are those for which $l \to l'$ in the "implication digraph" of a given satisfiability problem. How can we easily find all of the literals $l''$ such that $l'' \to l$, given $l$?

Verified: yes
Solve time: 56s

Solution

Let $D$ be the implication digraph of the given SAT instance. Its vertices are literals, and for every binary clause $(\bar{l} \lor l')$ there is a directed edge $l \to l'$. By definition of Algorithm L, $\mathrm{BIMP}(l)$ is the set of all literals reachable from $l$ in $D$.

The literals $l''$ satisfying $l'' \to l$ are exactly those from which there exists a directed path in $D$ ending at $l$. This is equivalent to reachability from $l$ in the digraph $D^{\mathrm{T}}$ obtained by reversing every edge of $D$. Indeed, a path

$l'' \to \cdots \to l$

in $D$ corresponds bijectively to a path

$l \to \cdots \to l''$

in $D^{\mathrm{T}}$.

Therefore the desired set is the same as $\mathrm{BIMP}_{D^{\mathrm{T}}}(l)$.

To compute it, one constructs the reverse adjacency lists of the implication digraph, that is, for each edge $u \to v$ in $D$ one stores an edge $v \to u$ in $D^{\mathrm{T}}$. Then a depth-first or breadth-first search starting at $l$ in $D^{\mathrm{T}}$ visits exactly all literals $l''$ such that $l'' \to l$ holds in $D$.

This yields all required literals using the same reachability procedure as $\mathrm{BIMP}$, applied to the transposed implication digraph. ∎