2-SAT via Implication Graphs

The previous lesson gave us strongly connected components: the maximal sets of vertices in a directed graph that can all reach one another, computable in $O(n+m)$ by a two-pass depth-first search. It is a beautiful algorithm, and this lesson is its most surprising payoff. We will take a problem that looks like it belongs to the world of intractable boolean satisfiability and show that one special case of it collapses to a single SCC computation.

The problem is 2-satisfiability (2-SAT). We are given $n$ boolean variables $x_1,\dots ,x_n$ and a formula in conjunctive normal form where every clause has exactly two literals, a literal being a variable $x_i$ or its negation $\neg x_i$:

We must decide whether some assignment of true/false to the variables makes every clause true at once, and if so, produce one. Allowing three literals per clause gives 3-SAT, which is NP-complete, the canonical hard problem we will meet in the intractability module. The jump from two literals to three is the jump from $O(n+m)$ to (as far as anyone knows) exponential. 2-SAT sits firmly in $\mathsf{P}$, and the reason is entirely graph-theoretic.¹

Reading a clause as two implications

The key observation is that a two-literal disjunction is logically the same as a pair of implications. The clause $(a\vee b)$ asserts that at least one of $a$, $b$ is true. So if $a$ happens to be false, $b$ is forced true; and symmetrically if $b$ is false, $a$ is forced. In symbols,

This rewriting is the whole idea. Build a directed implication graph $G$ on $2n$ vertices, one for each literal $x_i$ and one for its negation $\neg x_i$. For every clause $(a\vee b)$ in $\Phi$, add the two edges

An edge $u\to v$ reads if $u$ is true, then $v$ must be true. Because implication is transitive, a directed path $u⇝w$ means that committing to $u$ forces $w$: reachability in $G$ is exactly the relation forces. The graph is skew-symmetric by construction. The contrapositive $(\neg a\Rightarrow b)\equiv (\neg b\Rightarrow a)$ means every edge $u\to v$ has a mirror edge $\neg v\to \neg u$, and this symmetry is what makes the assignment step work.

The two highlighted edges are the implication pair of the clause $(\neg x_1\vee x_3)\equiv (x_1\Rightarrow x_3)\wedge (\neg x_3\Rightarrow \neg x_1)$. Mirror edges always come in such pairs.

When is the formula satisfiable?

A satisfying assignment must respect every forced implication: if it sets $u$ true and $u⇝v$, it must set $v$ true. The danger is a cycle of forcing that loops a literal back to its own negation. That danger is exactly an SCC.

The converse, that if no variable collides with its negation in an SCC then a satisfying assignment exists, is the more delicate half. We do not just assert it; the construction below builds an explicit assignment and the same skew-symmetry argument proves it consistent, which establishes the converse constructively.²

Constructing a satisfying assignment

Suppose the test passes: no $x_i$ and $\neg x_i$ share an SCC. Contract each SCC to a single super-vertex; the result is the condensation of $G$, which is always a directed acyclic graph (any cycle among components would have merged them). A DAG has a topological order, and topological order is what we assign by.

A two-pass SCC algorithm (Kosaraju or Tarjan) already numbers the components in a reverse topological order: Tarjan emits components sink-first, and Kosaraju's second pass discovers them in the order of decreasing first-pass finish time. So the comparison costs nothing extra: we set a literal true iff its component is discovered before its negation's in that reverse order (i.e. later topologically).

Why the rule is consistent. We must check the assignment never violates an implication edge, never sets some $u$ true and a forced $v$ false. Two facts make this automatic. First, edges of $G$ run from earlier components to later ones in topological order (that is what topological order means for a DAG), so an edge $u\to v$ has $\text{comp}(u)$ no later than $\text{comp}(v)$. Second, the skew-symmetry of $G$ guarantees that the condensation has a matching central symmetry: the component of $\neg u$ sits in the mirror position to the component of $u$. Concretely, if $u$'s component is topologically later than $\neg u$'s, so we set $u$ true, then for any edge $u\to v$ the mirror edge $\neg v\to \neg u$ forces $\neg v$'s component to be no later than $\neg u$'s, hence $v$'s component is no earlier than $u$'s, so $v$ is also assigned true. The edge is satisfied. No clause can be violated, and the converse of the theorem holds.³

Here $\neg x_1$ sits in an earlier component than $x_1$, so $x_1$ is set true (its SCC, highlighted, is later); likewise $\neg x_3$ precedes $x_3$, so $x_3$ is true. The whole pipeline (build $G$, run one SCC computation, scan the $n$ variables twice) is $O(n+m)$ time and space, matching the cost of the SCC algorithm it rests on.

Where 2-SAT shows up

The pattern to recognize is: each item has exactly two states, and the constraints are pairwise. Then every constraint becomes a two-literal clause and the whole problem becomes one implication graph. This covers a surprising range: placing labels on a map so adjacent labels do not collide (each label goes left-or-right), scheduling tasks each offered in one of two slots, two-coloring under these two must differ / must agree rules, and consistency checking in hardware and program verification, where 2-SAT is a standard subroutine. Pure 2-SAT rarely appears verbatim on LeetCode, but the implication-graph and pairwise- constraint shape is common: Satisfiability of Equality Equations is a union-find consistency check that is 2-SAT with only equalities and disequalities; Possible Bipartition asks for a two-coloring under must differ constraints, exactly the constraint-graph reduction; and Divide Nodes Into the Maximum Number of Groups layers a bipartiteness/BFS-distance argument on top. Knowing the implication-graph technique is what lets you see these as one family, and in competitive programming and formal verification 2-SAT in its raw form is common too.

Takeaways

• 2-SAT (CNF satisfiability with exactly two literals per clause) is solvable in $O(n+m)$, unlike NP-complete 3-SAT; the gap from two to three literals is the gap from polynomial to (conjecturally) exponential.
• Each clause $(a\vee b)$ is the implication pair $\neg a\Rightarrow b$ and $\neg b\Rightarrow a$; collecting them builds a skew-symmetric implication graph on the $2n$ literals, where reachability = forcing.
• Satisfiability theorem: $\Phi$ is satisfiable iff no variable shares an SCC with its own negation; a collision means $x\Rightarrow \neg x$ and $\neg x\Rightarrow x$, an outright contradiction.
• An assignment is read straight off the condensation DAG: set each literal true iff its SCC is topologically later than its negation's; skew-symmetry proves this never violates an implication edge.
• The whole algorithm is one strongly-connected-components computation plus two linear scans, a clean and surprising payoff of the SCC machinery from the previous lesson.