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: 1m03s

Solution

Let $F$ be a 2CNF formula with variables $x_1,\ldots,x_n$ and clauses $C_1,\ldots,C_m$, where each clause has the form $(l \lor l')$ with literals $l,l'$.

Algorithm L constructs the implication graph $D(F)$ whose vertex set consists of all literals ${x_1,\bar{x}_1,\ldots,x_n,\bar{x}_n}$. For each clause $(l \lor l')$ it introduces the two directed edges $\bar{l} \to l'$ and $\bar{l'} \to l$. This construction uses exactly two directed edges per clause, hence the total number of edges is $2m$.

The algorithm then computes the strongly connected components of $D(F)$, for instance by a depth-first search procedure that produces a component partition of the vertex set. Let $\mathcal{C}(v)$ denote the strongly connected component containing a vertex $v$.

If there exists a variable $x_i$ such that $\mathcal{C}(x_i) = \mathcal{C}(\bar{x}_i)$, then both literals lie on directed cycles reaching each other. In that case $x_i \to \bar{x}_i$ and $\bar{x}_i \to x_i$ are both implied by directed paths in $D(F)$. Any assignment that sets $x_i = 1$ forces $\bar{x}_i = 1$ by implication closure, contradicting the semantics of literals, and similarly setting $x_i = 0$ forces $x_i = 1$. Hence no satisfying assignment exists.

Conversely, assume that $\mathcal{C}(x_i) \ne \mathcal{C}(\bar{x}_i)$ for every $i$. Contract each strongly connected component into a single node, producing a directed acyclic graph $D^\ast(F)$. Define an assignment by processing components in reverse topological order of $D^\ast(F)$ and assigning each component a truth value as follows: when neither a component nor its complement has been assigned, assign the component to true and its complementary component to false. This is well-defined because if there is an edge $u \to v$ in $D(F)$ then $\mathcal{C}(u)$ precedes $\mathcal{C}(v)$ in the partial order, so assigning a component to true never forces a previously assigned component to change value. Each clause $(l \lor l')$ is satisfied because if both $\bar{l}$ and $\bar{l'}$ were assigned true, then both $l$ and $l'$ would be assigned false, contradicting the existence of edges $\bar{l} \to l'$ and $\bar{l'} \to l$ in the implication graph and the consistency of the component ordering. Therefore every clause has at least one true literal.

The running time is linear in $n+m$. The graph $D(F)$ has $2n$ vertices and $2m$ edges. The construction of all edges processes each clause once and performs $O(1)$ work per clause. The strongly connected component computation by depth-first search visits each vertex once and traverses each directed edge once, hence it performs $O(2n+2m)$ operations. The final assignment step processes each component once and each variable once, hence contributes $O(n)$ additional work. Therefore the total running time is $O(n+m)$.

Both correctness and the linear bound follow from the structure of implication paths and the fact that depth-first search partitions the graph into components in time proportional to its size. This completes the proof. ∎