↩ back to Graph Traversal

2-SAT (Two-Satisfiability)

The site's tenth graph traversal entry, and the first that doesn't start with a graph at all. A 2-SAT instance is a set of boolean variables and a set of clauses, each exactly two literals joined by or — a literal being a variable or its negation, like x₁ or ¬x₃. The question: is there an assignment of true/false to every variable that satisfies every clause at once? General boolean satisfiability (three or more literals per clause) is the textbook NP-complete problem — N-Queens and Graph Coloring elsewhere on this site both need real backtracking search because their underlying decision problems have no known shortcut. Capping every clause at exactly two literals removes that wall entirely: 2-SAT is decidable in O(V + E), by translating clauses into an implication graph and handing the actual work to Strongly Connected Components — a subroutine this site already built and verified, not a new traversal of its own.

Try it

Four variables, x₁ through x₄, each with a true node (top row) and a false node (bottom row, drawn as ¬x) in the implication graph. Build a clause from two literals and add it, or load one of the three examples below, then press Solve: the same Tarjan's-algorithm SCC routine from this site's own Strongly Connected Components page runs underneath, and the result is read straight off which component each literal lands in.

Why it works

A clause (a ∨ b) is satisfied exactly when at least one literal is true, which means: if a is false, b must be true, and symmetrically if b is false, a must be true. Both directions are genuine implications — ¬a → b and ¬b → a — and every clause contributes exactly those two directed edges to an implication graph over 2n nodes, one per literal. Crucially the two edges a single clause contributes are already contrapositives of each other (¬a → b is logically the same statement as ¬b → a), so nothing extra needs to be added by hand — every clause, translated once, carries its own contrapositive along for free.

Once every clause is translated, the formula is unsatisfiable if and only if some variable x has x and ¬x mutually reachable — each able to reach the other by following implication edges. One direction alone, x → ¬x, is completely ordinary: it just means "if x is true, so is ¬x's side of things," which is a real constraint but not yet a contradiction — it's satisfied by simply setting x false. Only a full round trip is fatal: x → … → ¬x and ¬x → … → x means assuming x true forces x false, and assuming it false forces it true — no assignment survives. Mutual reachability is exactly what a strongly connected component is, so the whole satisfiability question collapses to: run SCC on the implication graph, and check whether any variable's two literals landed in the same component.

When no variable fails that check, an assignment falls out of the SCC computation almost for free. This site's own Strongly Connected Components page establishes that Tarjan's algorithm closes components in reverse topological order of the condensation — sinks of the condensation DAG close first, sources last — and numbers them in that same closing order. Set variable x to true when its true-literal's component number is smaller than its false-literal's — meaning the true literal's component sits later in the condensation's real topological order, downstream of everything that could still imply its negation. Getting this comparison backwards doesn't crash anything and doesn't change whether the formula looks satisfiable — it just quietly hands back an assignment that fails its own clauses (see Pitfalls).

Reference implementation

Literal 2v is variable v true, literal 2v + 1 is variable v false. tarjanSCC is the same routine as the Strongly Connected Components page, written iteratively here to avoid a recursion-depth limit on large formulas:

function solve2SAT(n, clauses) {
  const negLit = (l) => l ^ 1;

  // build the implication graph: 2n nodes, two edges per clause
  const adj = Array.from({ length: 2 * n }, () => []);
  for (const [a, b] of clauses) {
    adj[negLit(a)].push(b); // ~a -> b
    adj[negLit(b)].push(a); // ~b -> a
  }

  const { comp } = tarjanSCC(adj); // comp[node] = SCC id, closing order (reverse topological)

  for (let v = 0; v < n; v++) {
    if (comp[2 * v] === comp[2 * v + 1]) {
      return { satisfiable: false, conflictVar: v }; // x and ~x mutually reachable
    }
  }

  const assignment = new Array(n);
  for (let v = 0; v < n; v++) {
    assignment[v] = comp[2 * v] < comp[2 * v + 1]; // true literal closes later in topological order
  }
  return { satisfiable: true, assignment };
}

Pitfalls

Adding only one direction of a clause's implication silently drops real constraints. It's tempting to add just ¬a → b and skip ¬b → a, reasoning that the clause is symmetric so one edge "should" cover it — it doesn't, because the two edges connect entirely different node pairs (one starts from ¬a, the other from ¬b) and dropping either one erases a real implication the formula actually requires. A 14,000-trial sweep across random clause sets (sizes 2 through 9 variables, checked against brute-force truth-table enumeration) found this version wrong on 943 of 14,000 trials (6.7%) — sometimes reporting a satisfiable formula as unsatisfiable, sometimes the reverse, depending on which half of the graph the missing edges would have connected.

Comparing the component numbers backwards produces a wrong assignment while still correctly saying "satisfiable." This is the subtler bug, and this page's own reference implementation was written with the comparison flipped on the first attempt, caught only once the generated assignment was checked against the actual clause list rather than trusted on sight. Same- component detection — the satisfiability verdict itself — doesn't depend on which side of the comparison means true, so a flipped rule sails through every "is this satisfiable" check and only fails the quieter "does this assignment actually satisfy every clause" check afterward. Across 15,761 satisfiable trials from the same sweep, the flipped comparison produced an assignment that failed at least one clause on 13,953 of them (88.5%) — wrong far more often than right, and never announced as wrong by the satisfiability check alone.

Checking one-directional reachability — does x reach ¬x at all — instead of requiring mutual reachability, over-reports contradictions that aren't there. A one-way path x → … → ¬x is an ordinary implication, not a contradiction; it only becomes fatal alongside a path back. Treating any forward reachability as fatal — the same 14,000-trial sweep used above, this time checking plain reachability instead of same-SCC-membership — reported the wrong verdict on 5,627 of 14,000 trials (40.2%), always in the same direction: real, satisfiable formulas wrongly condemned as contradictions the moment any implication chain happened to reach a variable's own negation without ever needing to loop back.

This is specifically about clauses capped at two literals. Dancing Links's own exact-cover reformulation and Graph Coloring's backtracking search both handle harder-shaped constraint problems on this site precisely because they don't get to assume anything like the two-literal structure that makes the implication graph — and therefore this shortcut — possible at all; three literals per clause (3-SAT) is enough to lose the shortcut and land back in NP-complete territory.

Complexity

Time: O(V + E) where V = 2n (one node per literal) and E = 2m (two directed edges per clause) — identical to plain Strongly Connected Components, since building the implication graph is itself only O(n + m) and everything past that point is the SCC computation, not an additional pass over it. Space: O(n + m) for the implication graph plus the SCC routine's own O(n) bookkeeping (discovery times, low-link values, the explicit stack). Checking every variable's two literals for a shared component afterward is a single O(n) pass. Deciding general boolean satisfiability with clauses of three or more literals has no known polynomial algorithm at all — the two-literal cap is what buys the entire linear-time result, not a smaller constant on the same kind of search.

This site's guide, Choosing a Graph Traversal Approach, compares this entry against the other ten Graph Traversal entries side by side.