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. This lesson is its most direct payoff: a problem that looks like intractable boolean satisfiability, but whose two-literal special case 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

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

where $a$ and $b$ range over literals and double negation cancels ($\neg \neg x$ is $x$). In figures we write $\bar{x}$ for $\neg x$. The construction rules, spelled out:

• Clause $(a\vee b)$ with two positive literals: edges $\bar{a}\to b$ and $\bar{b}\to a$. Nothing else — in particular not $a\to b$.
• Clause $(\neg a\vee b)$, i.e. the implication $a\Rightarrow b$: edges $a\to b$ and $\bar{b}\to \bar{a}$. Encoding an implication directly still produces two edges; the contrapositive comes along whether you write it or not.
• Clause $(\neg a\vee \neg b)$ (not both): edges $a\to \bar{b}$ and $b\to \bar{a}$.
• Unit clause $(a)$: treat it as $(a\vee a)$, contributing the single edge $\bar{a}\to a$, which forces $a$ true (we will see why in a moment).
• Constraint $x$ and $y$ must differ: two clauses $(x\vee y)$ and $(\neg x\vee \neg y)$, four edges; must agree is $(x\vee \neg y)$ and $(\neg x\vee y)$.

Every clause thus contributes exactly two edges (a duplicated edge for a unit clause), so the graph has $2n$ vertices and $2m$ 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 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.

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 failure mode is a cycle of forcing that loops a literal back to its own negation — and such a cycle is exactly an SCC.

The no collision test is a decision procedure — it answers satisfiable? — so its correctness splits into the two halves we named in the foundations: the test must never report satisfiable when no assignment exists (soundness), and must never miss a formula that is satisfiable (completeness). The two directions of the iff give exactly these two guarantees. The forward direction below — a collision forces a contradiction — is completeness: every truly unsatisfiable formula does produce a collision, so a satisfiable one never gets rejected. The converse, built constructively in the next section, is soundness: when the test passes we exhibit an assignment that really satisfies $\Phi$, so a satisfiable verdict is never a false positive.

The converse, that if no variable collides with its negation in an SCC then a satisfying assignment exists, is the more delicate half. The construction below builds an explicit assignment, and the same skew-symmetry argument proves it consistent, establishing 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).

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.

A complete worked example

We run the pipeline once end to end. Take three variables and four clauses:

Build the implication graph. Each clause $(a\vee b)$ contributes $\bar{a}\to b$ and $\bar{b}\to a$. Working clause by clause (writing $\bar{x}$ for $\neg x$):

That is eight edges on the six literal-vertices $x_1,{\bar{x}}_1,x_2,{\bar{x}}_2,x_3,{\bar{x}}_3$:

Run SCCs. The edges close two directed triangles: ${\bar{x}}_1\to x_2\to {\bar{x}}_3\to {\bar{x}}_1$ is one strongly connected component, and $x_1\to x_3\to {\bar{x}}_2\to x_1$ is another. So

No variable meets its own negation: $x_1\in B$ while ${\bar{x}}_1\in A$, and likewise for $x_2$ and $x_3$. The collision test passes on all three variables, so $\Phi$ is satisfiable.

Read the assignment. The condensation has just two super-vertices, $A$ and $B$, joined by the cross edges ${\bar{x}}_1\to x_1$ and ${\bar{x}}_3\to x_1$, both running $A\to B$. So $B$ is topologically later (the sink). The rule assign true to whichever of $x_i$, ${\bar{x}}_i$ lies in the later SCC makes every variable read straight off which component holds its positive literal:

• $x_1\in B$ (later) $\Rightarrow$ $x_1=\text{true}$.
• $x_2\in A$ (earlier), so ${\bar{x}}_2\in B$ is later $\Rightarrow$ $x_2=\text{false}$.
• $x_3\in B$ (later) $\Rightarrow$ $x_3=\text{true}$.

Check it. The assignment $(x_1,x_2,x_3)=(\text{T},\text{F},\text{T})$ satisfies every clause: $(x_1\vee x_2)=\text{T}$, $(\neg x_1\vee x_3)=(\text{F}\vee \text{T})=\text{T}$, $(\neg x_2\vee \neg x_3)=(\text{T}\vee \text{F})=\text{T}$, and $(x_1\vee x_3)=\text{T}$. No search was needed.

For contrast, add the clause $(\neg x_1\vee \neg x_3)$ — forbidding $x_1$ and $x_3$ from both being true. Its edges $x_1\to {\bar{x}}_3$ and $x_3\to {\bar{x}}_1$ now run $B\to A$, and the graph already had the cross edges ${\bar{x}}_1\to x_1$ and ${\bar{x}}_3\to x_1$ running $A\to B$. Edges in both directions collapse $A$ and $B$ into a single strongly connected component containing all six literals — in particular $x_1$ and ${\bar{x}}_1$ together. Once that happens the collision test fires and the formula is correctly reported unsatisfiable — no assignment can honor $x_1$ or $x_2$, $x_1$ or $x_3$, not both $x_2$ and $x_3$, $x_1\Rightarrow x_3$, and not both $x_1$ and $x_3$ at once.

from __future__ import annotations

from typing import Generic, Hashable, NamedTuple, Optional, TypeVar

from graph import Graph

Variable = TypeVar("Variable", bound=Hashable)

class Literal(NamedTuple, Generic[Variable]):
  """
    A variable together with a sign: `negated=False` is the variable itself,\n
    `negated=True` is its logical negation.\n
  """
  variable: Variable
  negated: bool

  def __invert__(self) -> Literal[Variable]:
    """
      The complementary literal, so `~Literal(x, False)` is `Literal(x, True)`.\n
    """
    return Literal(self.variable, not self.negated)

class Clause(NamedTuple, Generic[Variable]):
  """
    A two-literal disjunction `(first or second)`.\n
  """
  first: Literal[Variable]
  second: Literal[Variable]

def _literal_key(literal: Literal[Variable]) -> tuple[Variable, bool]:
  """
    A hashable, graph-friendly label for a literal vertex.\n
  """
  return (literal.variable, literal.negated)

class TwoSat(Generic[Variable]):
  """
    A 2-SAT instance: a set of variables and two-literal clauses.\n
    Add clauses, then call `solve` to decide satisfiability and, when\n
    satisfiable, recover an assignment.\n
  """

  def __init__(self) -> None:
    self.variables: list[Variable] = []
    self._seen_variables: set[Variable] = set()
    self.clauses: list[Clause[Variable]] = []

  def add_variable(self, variable: Variable) -> None:
    """
      Register `variable` so it appears in any returned assignment, even\n
      when no clause mentions it.\n
    """
    if variable not in self._seen_variables:
      self._seen_variables.add(variable)
      self.variables.append(variable)

  def add_clause(
    self,
    first: Literal[Variable],
    second: Literal[Variable],
  ) -> None:
    """
      Add the clause `(first or second)`, registering both variables.\n
    """
    # register both literals' variables, then record the disjunction.
    self.add_variable(first.variable)
    self.add_variable(second.variable)
    self.clauses.append(Clause(first, second))

  def add_implication(
    self,
    premise: Literal[Variable],
    conclusion: Literal[Variable],
  ) -> None:
    """
      Add the constraint `premise => conclusion`, which as a clause is\n
      `(not premise or conclusion)`. A convenience for building instances\n
      directly from implications.\n
    """
    self.add_clause(~premise, conclusion)

  def _implication_graph(self) -> Graph[tuple[Variable, bool]]:
    """
      The directed implication graph on the 2n literal-vertices.\n
      Each clause (a or b) contributes the edges (not a -> b) and\n
      (not b -> a).\n
    """
    # one vertex per literal: the variable and its negation.
    graph: Graph[tuple[Variable, bool]] = Graph(directed=True)
    for variable in self.variables:
      graph.add_vertex(_literal_key(Literal(variable, False)))
      graph.add_vertex(_literal_key(Literal(variable, True)))

    # each clause (a or b) becomes (not a -> b) and (not b -> a).
    for clause in self.clauses:
      graph.add_edge(_literal_key(~clause.first), _literal_key(clause.second))
      graph.add_edge(_literal_key(~clause.second), _literal_key(clause.first))

    return graph

  def solve(self) -> Optional[dict[Variable, bool]]:
    """
      Decide satisfiability. Return a satisfying assignment as a mapping\n
      from variable to boolean, or None when the formula is unsatisfiable.\n
    """
    # component[label] is the SCC index in reverse topological order:
    # sinks of the condensation get the smallest indices (see scc helper).
    graph = self._implication_graph()
    component: dict[tuple[Variable, bool], int] = _strongly_connected_components(
      graph
    )

    assignment: dict[Variable, bool] = {}
    for variable in self.variables:
      positive_component: int = component[_literal_key(Literal(variable, False))]
      negative_component: int = component[_literal_key(Literal(variable, True))]

      # a variable colliding with its own negation in one SCC is a
      # contradiction (x => not x and not x => x): unsatisfiable.
      if positive_component == negative_component:
        return None

      # a literal is true when its SCC is topologically LATER than its
      # negation's; reverse-topo indexing makes "later" the smaller index.
      assignment[variable] = positive_component < negative_component
    return assignment

  def is_satisfiable(self) -> bool:
    """
      Whether any assignment satisfies every clause.\n
    """
    return self.solve() is not None

def _strongly_connected_components(
  graph: Graph[tuple[Variable, bool]],
) -> dict[tuple[Variable, bool], int]:
  """
    Tarjan's SCC algorithm: label each vertex with its component index.\n
    Tarjan emits components in reverse topological order of the\n
    condensation (sinks first), so the returned indices increase from sinks\n
    toward sources. The 2-SAT assignment rule relies on exactly that order.\n
    Runs in O(n + m) with an explicit stack to avoid recursion limits.\n
  """
  # per-vertex dfs numbering and the lowlink that detects SCC roots.
  index_of: dict[tuple[Variable, bool], int] = {}
  lowlink_of: dict[tuple[Variable, bool], int] = {}
  next_index: int = 0

  # the tentative-component stack plus its membership set and final labels.
  on_stack: set[tuple[Variable, bool]] = set()
  component_stack: list[tuple[Variable, bool]] = []
  component_of: dict[tuple[Variable, bool], int] = {}
  next_component: int = 0

  for start in graph.vertices:
    if start.label in index_of:
      continue

    # iterative depth-first search; each frame tracks how far we have
    # walked through the current vertex's outgoing edges.
    call_stack: list[tuple[tuple[Variable, bool], int]] = [(start.label, 0)]
    while call_stack:
      label, edge_position = call_stack[-1]
      vertex = graph.vertex(label)

      if edge_position == 0:
        index_of[label] = next_index
        lowlink_of[label] = next_index
        next_index += 1
        on_stack.add(label)
        component_stack.append(label)

      # advance through neighbors, descending into any unvisited one.
      descended: bool = False
      while edge_position < len(vertex.outgoing):
        neighbor_label = vertex.outgoing[edge_position].target.label
        edge_position += 1
        if neighbor_label not in index_of:
          call_stack[-1] = (label, edge_position)
          call_stack.append((neighbor_label, 0))
          descended = True
          break
        if neighbor_label in on_stack:
          lowlink_of[label] = min(lowlink_of[label], index_of[neighbor_label])
      if descended:
        continue

      # all neighbors processed: fold in finished children's lowlinks,
      # then if this vertex is a root, pop off its component.
      call_stack.pop()
      if call_stack:
        parent_label = call_stack[-1][0]
        lowlink_of[parent_label] = min(
          lowlink_of[parent_label], lowlink_of[label]
        )
      if lowlink_of[label] == index_of[label]:
        while True:
          member = component_stack.pop()
          on_stack.discard(member)
          component_of[member] = next_component
          if member == label:
            break
        next_component += 1

  return component_of

from collections.abc import Hashable, Iterator
from typing import Generic, Optional, TypeVar


Label = TypeVar("Label", bound=Hashable)


class Edge(Generic[Label]):
  """
    A directed connection from `source` to `target`, carrying a weight.\n
  """

  def __init__(
    self,
    source: Vertex[Label],
    target: Vertex[Label],
    weight: float = 1.0,
  ) -> None:
    self.source: Vertex[Label] = source
    self.target: Vertex[Label] = target
    self.weight: float = weight

  def __repr__(self) -> str:
    return f"Edge({self.source.label!r} -> {self.target.label!r}, w={self.weight})"


class Vertex(Generic[Label]):
  """
    A graph vertex: a label plus the list of edges leaving it.\n
  """

  def __init__(self, label: Label) -> None:
    self.label: Label = label
    self.outgoing: list[Edge[Label]] = []

  def neighbors(self) -> list[Vertex[Label]]:
    """
      The vertices reachable from this one by a single edge.\n
    """
    return [edge.target for edge in self.outgoing]

  def edge_to(self, label: Label) -> Optional[Edge[Label]]:
    """
      The outgoing edge to the vertex with `label`, or None.\n
    """
    for edge in self.outgoing:
      if edge.target.label == label:
        return edge
    return None

  def __repr__(self) -> str:
    return f"Vertex({self.label!r})"


class Graph(Generic[Label]):
  """
    A graph of Vertex objects linked by Edge objects.\n
    Pass `directed=True` for a digraph; otherwise each `add_edge` inserts\n
    the reverse edge too.\n
  """

  def __init__(self, directed: bool = False) -> None:
    self.directed: bool = directed
    self._vertices: dict[Label, Vertex[Label]] = {}

  def add_vertex(self, label: Label) -> Vertex[Label]:
    """
      Return the vertex for `label`, creating it if it is absent.\n
    """
    # reuse the existing vertex, or mint and register a fresh one.
    vertex = self._vertices.get(label)
    if vertex is None:
      vertex = Vertex(label)
      self._vertices[label] = vertex
    return vertex

  def add_edge(
    self,
    source_label: Label,
    target_label: Label,
    weight: float = 1.0,
  ) -> None:
    """
      Connect two labels (creating either vertex as needed).\n
      Adds the reverse edge as well when the graph is undirected.\n
    """
    source = self.add_vertex(source_label)
    target = self.add_vertex(target_label)

    # link source to target, and mirror it back when undirected.
    source.outgoing.append(Edge(source, target, weight))
    if not self.directed:
      target.outgoing.append(Edge(target, source, weight))

  def vertex(self, label: Label) -> Vertex[Label]:
    """
      The vertex carrying `label` (raises KeyError if absent).\n
    """
    return self._vertices[label]

  @property
  def vertices(self) -> list[Vertex[Label]]:
    """
      Every vertex, in insertion order.\n
    """
    return list(self._vertices.values())

  @property
  def labels(self) -> list[Label]:
    """
      Every vertex label, in insertion order.\n
    """
    return list(self._vertices)

  def edges(self) -> Iterator[Edge[Label]]:
    """
      Each edge once — an undirected edge is yielded a single time.\n
    """
    # track undirected endpoint pairs so each is emitted only once.
    seen: set[frozenset[Label]] = set()

    for vertex in self._vertices.values():
      for edge in vertex.outgoing:
        # skip an undirected edge already yielded from the other endpoint.
        if not self.directed:
          endpoints = frozenset((edge.source.label, edge.target.label))
          if endpoints in seen:
            continue
          seen.add(endpoints)

        yield edge

  def __contains__(self, label: Label) -> bool:
    return label in self._vertices

  def __iter__(self) -> Iterator[Vertex[Label]]:
    return iter(self._vertices.values())

  def __len__(self) -> int:
    return len(self._vertices)

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 wide 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. The implication-graph technique unifies these as one family, and in competitive programming and formal verification 2-SAT in its raw form is common too.

The boundary of tractability

2-SAT is a boundary case: almost any modification of the problem is NP-hard.

The canonical linear algorithm. The implication-graph reduction and the later SCC wins assignment rule are due to Aspvall, Plass, and Tarjan (1979), who packaged the whole thing as a single $O(n+m)$ procedure.⁴ Their paper actually solves the more general quantified 2-SAT, but strip the quantifiers and what remains is the algorithm here: build $G$, one SCC pass, two scans. It remains the standard method, used verbatim in competitive programming and as a subroutine in SAT solvers' preprocessing.

Randomized 2-SAT. A different linear-expected-time algorithm ignores the graph entirely. Papadimitriou's random-walk method starts from any assignment and, while some clause is unsatisfied, picks one and flips a uniformly random one of its two literals.⁵ Each flip is a step in a random walk on the number of variables that agree with a fixed satisfying assignment; because a two-literal clause guarantees at least a $\frac{1}{2}$ chance of stepping toward the target, the walk reaches a satisfying assignment in $O(n^2)$ expected flips. The same idea with three literals only steps toward the target with probability $\frac{1}{3}$, and the walk drifts — this is why Schöning's randomized 3-SAT algorithm runs in exponential (though better-than-brute-force) time.

Everything nearby is hard. The two-to-three-literal boundary is the most famous, but not the only one:

• 3-SAT is NP-complete (Cook-Levin), the archetypal hard problem of the intractability module.
• MAX-2-SAT — satisfy as many clauses as possible when you cannot satisfy them all — is NP-hard even though plain 2-SAT is easy; the Goemans-Williamson semidefinite-programming relaxation gives the best known approximation.
• Weighted / quantified variants and counting the number of satisfying assignments (#2-SAT) are all intractable.

2-SAT is a different problem from general SAT, not merely a smaller one: its special structure (every clause is an implication, so forcing is a reachability relation) is what collapses it into a graph question. Without that structure the problem is NP-hard.

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 direct payoff of the SCC machinery from the previous lesson.