TAOCP 7.2.2.2 Exercise 135
The implication digraph has a vertex for every literal.
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: 1m20s
Solution
The implication digraph has a vertex for every literal. By definition, the literals $l'$ in $\operatorname{BIMP}(l)$ are exactly the out-neighbors of $l$, namely the literals satisfying
$l \to l'.$
To find all literals $l''$ satisfying
$l'' \to l,$
we need the in-neighbors of $l$ in the same digraph. The direct way to obtain them is to store the implication lists in the reverse direction as well.
For every implication
$l \to l',$
insert $l$ into a reverse list associated with $l'$. Thus, in addition to the table $\operatorname{BIMP}(l)$, maintain a table, say $\operatorname{RBIMP}(l)$, defined by
$\operatorname{RBIMP}(l)={l'':l''\to l}.$
During construction of the implication graph, whenever a clause produces an implication from $a$ to $b$, the construction performs the two insertions
$$ \operatorname{BIMP}(a)\leftarrow b, $$
and
$$ \operatorname{RBIMP}(b)\leftarrow a. $$
After these lists have been built, the desired literals for a given $l$ are obtained by scanning $\operatorname{RBIMP}(l)$. Each element $l''$ encountered there satisfies $l''\to l$ by the definition of the reverse table, and every literal implying $l$ was inserted into this list when its corresponding implication was created.
Therefore the required set is
$$ \boxed{\operatorname{RBIMP}(l)={l'':l''\to l}}. $$
This requires only constant additional work per implication during graph construction, and then a query for a particular $l$ takes time proportional to the number of literals that imply $l$.