TAOCP 7.2.2.2 Exercise 162
Let the clauses of $F$ be stored so that, for every literal $l$, we have a list $\mathcal C(l)$ of all clauses containing $l$.
Section 7.2.2.2: Satisfiability
Exercise 162. [21] [21] Devise an efficient way to discover all of the (a) blocked binary clauses ($\bar{l} \vee a$) and (b) size-two autarkies $A = {a, a'}$ of a given kSAT problem $F$.
Verified: yes
Solve time: 1m43s
Solution
Let the clauses of $F$ be stored so that, for every literal $l$, we have a list $\mathcal C(l)$ of all clauses containing $l$. The construction of these lists requires one pass through the input. During this pass, a clause $C$ contributes itself to $\mathcal C(l)$ for every literal $l\in C$.
For a binary clause $(\bar l\vee a)$, the clause is blocked if the literal $l$ is a blocking literal. By the definition of blocking, every resolvent of $(\bar l\vee a)$ with a clause containing $l$ must be tautological. Let $D$ be any clause in $\mathcal C(l)$. The resolvent on $l$ is
$$ (D\setminus{l})\cup{a}. $$
Because the input clauses contain strictly distinct literals, this resolvent is tautological exactly when $D$ contains $\bar a$. Hence
$$ (\bar l\vee a)\text{ is blocked} \iff \forall D\in\mathcal C(l),\quad \bar a\in D . $$
Therefore the discovery of all blocked binary clauses can be reduced to finding, for every pair of literals $(l,a)$, whether every member of $\mathcal C(l)$ contains $\bar a$.
For each literal $l$, initialize a counter $N_l$ equal to the number of clauses in $\mathcal C(l)$. For each literal $a$, initialize a counter $N_{l,a}$ equal to the number of clauses in $\mathcal C(l)$ that contain $\bar a$. These counters can be obtained by scanning the clauses. A binary clause $(\bar l\vee a)$ is blocked precisely when
$$ N_{l,a}=N_l . $$
The algorithm then examines each binary clause of $F$. If its literals are $\bar l$ and $a$, it outputs the clause whenever the equality above holds. The test is constant time after the counters have been constructed. The total work is linear in the number of literal occurrences for the construction of the tables, plus linear in the number of binary clauses for the final scan.
For size-two autarkies, let
$$ A={a,a'} $$
where $a$ and $a'$ are strictly distinct literals. The set $A$ is an autarky exactly when every clause containing either complementary literal $\bar a$ or $\bar {a'}$ is already satisfied by at least one member of $A$. Equivalently, for every clause $C$,
$$ \bar a\in C\ \Longrightarrow\ a\in C\ \text{or}\ a'\in C, $$
and
$$ \bar {a'}\in C\ \Longrightarrow\ a\in C\ \text{or}\ a'\in C . $$
The first condition says that no clause contains $\bar a$ while avoiding both literals in $A$. Since the clauses are strictly distinct, this is equivalent to saying that every clause in $\mathcal C(\bar a)$ contains $a'$ unless it already contains $a$. The second condition is the analogous statement with $a$ and $a'$ interchanged.
For each literal $a$, define
$$ S(a)={C\in F:\bar a\in C,\ a\notin C}. $$
Thus $S(a)$ is the collection of clauses that would be unsatisfied by setting $a$ true. The pair ${a,a'}$ is a size-two autarky exactly when
$$ S(a)\subseteq \mathcal C(a') \quad\text{and}\quad S(a')\subseteq \mathcal C(a). $$
The sets $S(a)$ can be constructed from the same occurrence lists used above. For every candidate pair of literals $a,a'$ with different variables, the two subset tests determine whether ${a,a'}$ is an autarky. The tests can be performed efficiently by representing the clause occurrence sets as bit vectors. If there are $M$ clauses, each subset test costs $O(M/w)$ machine operations on words of size $w$, so all pairs can be tested in $O(n^2M/w)$ time for $n$ variables. The preprocessing requires only one scan of the formula.
The correctness of the blocked-clause procedure follows from the equivalence
$$ (\bar l\vee a)\text{ blocked} \iff \forall D\in\mathcal C(l),\ \bar a\in D, $$
because the right-hand side is exactly the condition that every possible resolvent on $l$ contains both $a$ and $\bar a$.
The correctness of the autarky procedure follows from the definition of an autarky. If both subset conditions hold, every clause affected by the partial assignment $A$ contains a literal of $A$, so $A$ satisfies all affected clauses. Conversely, if ${a,a'}$ is an autarky and a clause belongs to $S(a)$, that clause contains $\bar a$ and does not contain $a$; it must therefore contain $a'$ to be satisfied by $A$. Hence $S(a)\subseteq\mathcal C(a')$. The same argument gives $S(a')\subseteq\mathcal C(a)$, so the two tests find every size-two autarky and no others.
This completes the proof.
∎