TAOCP 7.2.2.2 Exercise 170

Exercise 170. [25] (Marijn Heule, 2013.) Show that Algorithm L solves 2SAT in linear time.

Verified: no
Solve time: 3m17s

Solution

Let the input formula be a 2SAT formula $F$ with $n$ variables and $m$ clauses. Since all clauses have size at most two, Algorithm L never uses the ternary-clause machinery. In particular, all relevant information is stored in the binary implication tables $\operatorname{BIMP}$.

A binary clause

$$ (u\vee v) $$

is represented by the two implications

$$ \bar u\rightarrow v,\qquad \bar v\rightarrow u . $$

Algorithm L stores exactly these implications: $v$ occurs in $\operatorname{BIMP}(\bar u)$, and $u$ occurs in $\operatorname{BIMP}(\bar v)$. Thus the total initial size of all BIMP tables is $2m$.

The key point is that, for a 2SAT instance, every inference made by Algorithm L is a binary implication inference. Consider step L5. If a literal $l$ is placed in the FORCE array, the binary propagation routine repeatedly scans $\operatorname{BIMP}(l)$. Whenever it finds a literal $u$ with

$$ l\rightarrow u , $$

it places $u$ in the propagation stack unless $u$ has already been assigned. A contradiction is found exactly when the propagation process assigns both $x$ and $\bar x$ for some variable $x$.

Therefore, after a set $S$ of literals has been accepted, step L5 computes the implication closure

$$ \operatorname{cl}(S)={u:S\rightarrow u}. $$

For a 2SAT formula, this closure is the only possible source of deductions. There are no ternary clauses that could create new binary clauses, so steps L7 through L9 are never executed. The only changes to the BIMP tables are those made by initialization and by possible bookkeeping during lookahead, and the original implication information is never altered by a real assignment.

We now analyze the recursion. Suppose Algorithm L reaches step L3 and chooses a literal $l$ on which to branch. The two possible branches are

$$ l=1 $$

and

$$ \bar l=1 . $$

The first branch performs exactly the implication closure of $l$, and the second performs exactly the implication closure of $\bar l$. If the first branch reaches a contradiction, then the closure of $l$ contains some literal together with its complement. Hence $l$ cannot occur in any satisfying assignment. Consequently every satisfying assignment must satisfy $\bar l$. Thus, after the failed branch, the second branch is forced and no further branching on the same variable can occur.

The same argument applies recursively. A branch can fail only after the branch literal has been proved impossible by implication propagation. Hence a failed branch permanently removes one possible value of a variable. A successful branch fixes that variable and continues only on variables that have not yet been fixed.

It remains to bound the total amount of propagation. Let a variable become fixed when one of its literals enters the stack $R$. Because Algorithm L maintains the list of fixed variables and restores the data structures only when backtracking, each variable can become fixed once on a path from the root to a leaf. If a branch is rejected, the rejected literal is never considered again: its opposite value is forced by the contradiction. Therefore the search tree of Algorithm L on a 2SAT instance has at most one successful continuation after every failed branch, and the total number of branch decisions is bounded by the number of variables.

Now charge the work performed by propagation. During a propagation step, Algorithm L scans the BIMP list of a literal only when that literal is newly accepted as true. Since each accepted literal corresponds to fixing one of the $2n$ possible literal values, each BIMP entry is examined only a constant number of times during the whole execution. The total number of BIMP entries is

$$ 2m . $$

The remaining work consists of maintaining the stacks $R$, FORCE, and the variable lists. Each literal insertion, deletion, or restoration is charged to the corresponding literal occurrence or variable, so this work is

$$ O(n+m). $$

The initialization also takes linear time. Constructing the BIMP tables requires reading each clause once and inserting at most two implication entries per clause, giving

$$ O(n+m) $$

time and space.

Thus Algorithm L does not need to be replaced by a separate strongly connected component algorithm. Its own binary propagation mechanism, together with the fact that every unsuccessful branch proves one literal impossible and never repeats that work, guarantees that the complete backtracking search has only linear total cost on 2SAT instances.

Therefore Algorithm L decides every 2SAT instance in

$$ \boxed{O(n+m)} $$

time. $\square$