2-SAT

Convert two-literal clauses into implications, group them by SCC, and derive a satisfying assignment.

Core idea

Clause a or b is equivalent to two implications: not a implies b, and not b implies a. Strongly connected components expose contradictions and provide an assignment order.

Read the visualization

Each variable appears as two literal vertices. Clause edges arrive in pairs, SCC colors group mutual implications, and the final badges show the selected truth values.

Create one implication-graph vertex for every literal and its negation.

1function twoSat(n: number, clauses: [number, number][]): boolean[] | null {
const g: number[][] = Array.from({ length: 2 * n }, () => []); // 2n  literal init node,  implication init empty 
for (const [a, b] of clauses) {                 // init clause init count  implication  edge 
  g[a ^ 1].push(b);                             // ¬a → b
  g[b ^ 1].push(a);                             // ¬b → a
}
const comp = tarjan(2 * n, g);                  // Tarjan  compute  SCC( number   7 scc), comp=scc
for (let v = 0; v < n; v++)                     //  verdict: x  and  ¬x scc group  ⟺  no solution 
  if (comp[2 * v] === comp[2 * v + 1]) return null;
const assign: boolean[] = [];
for (let v = 0; v < n; v++)                     // assign value:  take assign literal assign as  true 
  assign.push(comp[2 * v] < comp[2 * v + 1]);
return assign;                                  // done solution 
14}

variable: 3(A,B,C)
clause: (A∨B) ∧ (A∨¬B) ∧ (A∨C) ∧ (¬A∨¬B)
implication edge: 0 / 8

Complexity and tradeoffs

Time: O(V+E). Space: O(V+E). A formula is impossible exactly when a variable and its negation share one strongly connected component.

Invariant: A partial implication graph represents exactly the clauses already inserted; a variable is contradictory only if both literals enter one SCC.

Where it fits

2-SAT models pairwise choices, scheduling exclusions, orientation constraints, and configuration flags. Clauses with three or more unrestricted literals make the general problem NP-complete.