Pattern Guide
2-SAT
"Solve boolean formulas with 2-literal clauses in O(V+E) via SCC."
2-SAT solves boolean satisfiability problems where each clause has exactly 2 literals. Build an implication graph: (¬x → y) and (¬y → x) for clause (x ∨ y). A valid assignment exists iff no variable x is in the same SCC as ¬x. Find SCCs (Kosaraju/Tarjan), topological-order SCC index assigns truth values. Essential for scheduling, graph coloring, and constraint satisfaction problems.
16 min readgraph problems →
Problems you can solve with this pattern
3 problems · click any to start solving
2-SAT with Kosaraju's SCC
class TwoSAT {
constructor(n) {
this.n = n; // number of variables
this.adj = Array.from({length: 2*n}, () => []);
this.radj = Array.from({length: 2*n}, () => []);
}
// Add clause (x ∨ y) where literals: variable i = i, negation = i+n
addClause(x, y) {
// ¬x → y and ¬y → x
const negX = x < this.n ? x + this.n : x - this.n;
const negY = y < this.n ? y + this.n : y - this.n;
this.adj[negX].push(y); this.radj[y].push(negX);
this.adj[negY].push(x); this.radj[x].push(negY);
}
solve() {
const n2 = 2 * this.n;
const order = [], visited = new Array(n2).fill(false);
const dfs1 = (v) => {
visited[v] = true;
for (const u of this.adj[v]) if (!visited[u]) dfs1(u);
order.push(v);
};
for (let i = 0; i < n2; i++) if (!visited[i]) dfs1(i);
const comp = new Array(n2).fill(-1);
let numComp = 0;
const dfs2 = (v, c) => {
comp[v] = c;
for (const u of this.radj[v]) if (comp[u] === -1) dfs2(u, c);
};
for (let i = n2 - 1; i >= 0; i--) {
if (comp[order[i]] === -1) dfs2(order[i], numComp++);
}
// Check satisfiability and extract assignment
const vals = new Array(this.n);
for (let i = 0; i < this.n; i++) {
if (comp[i] === comp[i + this.n]) return null; // unsatisfiable
vals[i] = comp[i] > comp[i + this.n]; // higher comp = later in topo = TRUE
}
return vals;
}
}
// Usage:
// const sat = new TwoSAT(n);
// sat.addClause(x, y) -- (var_x OR var_y)
// sat.addClause(x, x+n) -- forces var_x to be TRUE (x OR NOT x is tautology, but: x AND ¬¬x = x)
// For "var x must be true": addClause(x, x) if using literal encoding
// const result = sat.solve(); // null = unsat, array = assignment2-SAT encodes each clause (A ∨ B) as two implications: (¬A → B) and (¬B → A). Variable i has two nodes: i (true) and i+n (false/negated). Build directed implication graph. Find SCCs with Tarjan's or Kosaraju's. Satisfiable iff no variable i has scc[i] == scc[i+n]. Assign: if scc[i] > scc[i+n] in topological order, variable i is TRUE.
2-SAT with Kosaraju's SCC
class TwoSAT {
constructor(n) {
this.n = n; // number of variables
this.adj = Array.from({length: 2*n}, () => []);
this.radj = Array.from({length: 2*n}, () => []);
}
// Add clause (x ∨ y) where literals: variable i = i, negation = i+n
addClause(x, y) {
// ¬x → y and ¬y → x
const negX = x < this.n ? x + this.n : x - this.n;
const negY = y < this.n ? y + this.n : y - this.n;
this.adj[negX].push(y); this.radj[y].push(negX);
this.adj[negY].push(x); this.radj[x].push(negY);
}
solve() {
const n2 = 2 * this.n;
const order = [], visited = new Array(n2).fill(false);
const dfs1 = (v) => {
visited[v] = true;
for (const u of this.adj[v]) if (!visited[u]) dfs1(u);
order.push(v);
};
for (let i = 0; i < n2; i++) if (!visited[i]) dfs1(i);
const comp = new Array(n2).fill(-1);
let numComp = 0;
const dfs2 = (v, c) => {
comp[v] = c;
for (const u of this.radj[v]) if (comp[u] === -1) dfs2(u, c);
};
for (let i = n2 - 1; i >= 0; i--) {
if (comp[order[i]] === -1) dfs2(order[i], numComp++);
}
// Check satisfiability and extract assignment
const vals = new Array(this.n);
for (let i = 0; i < this.n; i++) {
if (comp[i] === comp[i + this.n]) return null; // unsatisfiable
vals[i] = comp[i] > comp[i + this.n]; // higher comp = later in topo = TRUE
}
return vals;
}
}
// Usage:
// const sat = new TwoSAT(n);
// sat.addClause(x, y) -- (var_x OR var_y)
// sat.addClause(x, x+n) -- forces var_x to be TRUE (x OR NOT x is tautology, but: x AND ¬¬x = x)
// For "var x must be true": addClause(x, x) if using literal encoding
// const result = sat.solve(); // null = unsat, array = assignment2-SAT encoding rules:
- Clause (x ∨ y): add (¬x → y) and (¬y → x)
- Force x to be TRUE: add clause (x ∨ x), i.e., single implication (¬x → x)
- Force x to be FALSE: add clause (¬x ∨ ¬x)
- x implies y: add (x → y) and (¬y → ¬x)
Assignment rule: After Kosaraju's, variable x is TRUE if SCC(x) appears later in topological order than SCC(¬x).
Applications: Scheduling with conflicts, graph 2-coloring with constraints, circuit satisfiability, constraint satisfaction problems reducible to 2-literal form.
- Clause (x ∨ y): add (¬x → y) and (¬y → x)
- Force x to be TRUE: add clause (x ∨ x), i.e., single implication (¬x → x)
- Force x to be FALSE: add clause (¬x ∨ ¬x)
- x implies y: add (x → y) and (¬y → ¬x)
Assignment rule: After Kosaraju's, variable x is TRUE if SCC(x) appears later in topological order than SCC(¬x).
Applications: Scheduling with conflicts, graph 2-coloring with constraints, circuit satisfiability, constraint satisfaction problems reducible to 2-literal form.