2-CNF Satisfiability is Poly-time Decidable

2-CNF is CNF that every clause has at most two literals. The satisfiability of CNF is NP-complete in general, however 2-CNF satisfiability is special becuase it is solvable in polynomial time. Let’s call the satisfiability problem of 2-CNF as 2-SAT.

Definition. (complement) For literal $L$, define its complement $\overline{L}$ as following:

\[\overline{L} := \begin{cases} p & \text{if } L = \neg p. \\ \neg p & \text{if } L = p. \end{cases}\]

Definition. (implication graph) The implication graph of a 2-CNF formula $F$ is a directed graph $G = (V, E)$. For propositional variables $p_1, \cdots, p_n$,

\[V := \{p_1, \cdots, p_n\} \cup \{\neg p_1, \cdots, \neg p_n\}\] \[E = \{(L, M) : \text{clause } ( \overline{L} \vee M ) \text{ or } (L \vee \overline{M}) \text{ appears in } F \}\]

The edge (L, M) represents the implication $L \to M$. For example, consider following 2-CNF formula.

\[(p_0 \vee p_2) \wedge (p_0 \vee \neg p_3) \wedge (p_1 \vee \neg p_3) \wedge (p_1 \vee \neg p_4) \wedge (p_2 \vee \neg p_4) \\ \wedge (p_0 \vee \neg p_5) \wedge (p_1 \vee \neg p_5) \wedge (p_2 \vee \neg p_5) (p_3 \vee p_6) \wedge (p_4 \vee p_6) \wedge (p_5 \vee p_6)\]

Then we can draw an implication graph as follows.

Figure 2. Example implication graph

For instance, the formula has $(p_0 \vee p_2)$ clause, then there are two implications, $\neg p_0 \to p_2$ and $\neg p_2 \to p_0$. These two edges exists in the graph.

Definition. (consistent) Implication graph is consistent if there is no propositional variable $p$ with paths from $p \to \neg p$ and $\neg p \to p$.

In other words, the formula $F$ is consistent if its implication graph has no $p$ that cycle having nodes $p$ and $\neg p$ exists.

Theorem. There is polynomial time algorithm that checks if implication graph $G$ is consistent.

It is well-known that we can build strongly connected components from directed graph $G$ in polynomial time. Also, checking if there is a component containing $p$ and $\neg p$ for arbitrary variable $p$ takes linear time.

Finally, we can show 2-SAT is solvable in polynomial time if we show the following.

Theorem. 2-CNF formula $F$ is satisfiable iff its implication graph $G$ is consistent.

($\Rightarrow$) This direction is quite trivial. Suppose $F$ is satisfiable, and implication graph $G$ is not consistent. Then there exists an satisfying assignment $A \models F$. If $G$ is not consistent, a propositional variable $p$ such that implications $p \to \neg p$ and $\neg p \to p $ holds. If $A(p) = true$, then $p \to \neg p$ does not hold. If $A(p) = false$, then $\neg p \to p$ does not hold. Contradiction.

($\Leftarrow$) We need to show that if implication graph is consistent, then the formula is satisfiable. Claim that following algorithm always return satisfying assignment if $G$ is consistent.

    \begin{algorithm}
    \caption{2-SAT}
    \begin{algorithmic}
    \INPUT{2-CNF $F$}
    \PROCEDURE{2-SAT}{$F$}
        \STATE $A :=$ empty assignment
        \WHILE{there is some unassigned variable}
            \STATE pick an unassigned literal $L$ which there is no path from $L$ to $\overline{L}$
            \STATE set $A(L) := 1$ and $A(\overline{L}) := 0$
            \WHILE{ $\exists (M, N) \in E$ with $A(M) = 1$ and $A(N)$ is undefined}
                \STATE $A(N) := 1$ and $A(\overline{N}) := 0$
            \ENDWHILE
        \ENDWHILE
        \RETURN{$A$}
    \ENDPROCEDURE
    \end{algorithmic}
    \end{algorithm}

Empty assignment means, $A(p)$ is not defined for every assignment $p$. To prove this algorithm works, we will show two invariants first.

• Outer loop invariant $I1$ : Any node reachable from a true node is also true.
  • (base) $I1$ is true for empty assignment.
  • (step) If $I1$ holds and there is some assigned variable, we can always choose a literal $L$ such that there is no path $L \to \overline{L}$ by consistency. After running inner loop, there is no path $true \to false$ (assumming the $I2$) and and there is no edge $true \to undefined$ (inner loop condition). Therefore, $I1$ holds after running outer loop body.
• Inner loop invariant $I2$ : There is no path from a true node to a false node.
  • (base) Suppose $I2$ is not true at the beginning of the inner loop. By $I1$, every node reachable from a true node is also true at the beginning of the outer loop. Therefore, there is no path neither $true \to undefined$ nor $true \to false$ at the beginning of the outer loop. Since $I2$ is breaked after $A(L) := 1$, there is a path $L \to X$ where $A(X) = 0$. From the fact that there is no path from $L$ to $\overline{L}$, so we know $X \ne \overline{L}$. Then $X$ is the literal that was assigned as false at the begnning of the outer loop body. By contrapositive of $L \to X$, there is a path $\overline{X} \to \overline{L}$, which is a path from true to false. However, $\overline{X}$ is assigned as true at the begnning of the outer loop, so this contradicts to $I1$. Therefore the assumption is false.

Figure 2. Contradiction by contrapositive

• (step) Assume $I2$ is true at the beginning of the inner loop. After running inner loop body, suppose $I2$ does not hold. There exist a path $P$ from true to false.

If outer loop invariant is true and all variables are assigned, then for all implications $M \to N$, there is no case that $A(M) = 1$ and $A(N) = 0$.