2-CNF Satisfiability is Poly-time Decidable

Mar. 20, 2023

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.

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.

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.

(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$ .