38.05Intermediate / Advanced4 topics16 min4 interactive animations

2-SAT

2-SAT asks whether a formula made of two-literal clauses can be satisfied. Each clause becomes two implications, and the formula is satisfiable exactly when no variable shares a component with its negation.

Learning goals

Turn a clause (a or b) into two implications
Encode variables and negations as graph vertices
Decide satisfiability from the SCCs
Construct a satisfying assignment from the component order

Prerequisites

Strongly connected componentsBoolean logic

Seating plans, scheduling rules and compatibility choices often come as “either A or B” rules. Every rule says that if one choice is false the other is forced: a chain of forced choices is a path in a graph.

38.05.1

Implication graph

A **2-SAT** formula is a conjunction of clauses, each an OR of two literals (a variable or its negation), for example (x1 ∨ ¬x2) ∧ (¬x1 ∨ x3). We want an assignment of true/false to the variables that makes every clause true.

A clause (a ∨ b) says: if a is false then b must be true, and if b is false then a must be true. That is two **implications**, ¬a → b and ¬b → a, and they are equivalent to the clause. Put each as an arrow in a directed graph on the literals. A path l1 → l2 → ... → lk then means: if l1 is true, every literal on it is forced true.

The “Satisfiable” preset (1,2 -1,3 -2,-3 -1,-2, three variables) has 6 literal vertices and 8 arrows: 4 clauses, 2 implications each. Every arrow comes with its mirror image: a → b is always accompanied by ¬b → ¬a. That symmetry is what makes the SCC test below correct.

Java

1@SuppressWarnings("unchecked")
2static List<Integer>[] implicationGraph(int n, int[][] clauses) {   // literal l: variable l / 2, negated when l is odd
3    List<Integer>[] g = new List[2 * n];
4    for (int i = 0; i < 2 * n; i++) g[i] = new ArrayList<>();
5    for (int[] c : clauses) {                            // clause {a, b} means (a or b)
6        g[c[0] ^ 1].add(c[1]);                           // not a  ->  b
7        g[c[1] ^ 1].add(c[0]);                           // not b  ->  a
8    }
9    return g;
10}

2-SAT: implication graph, SCCs and the assignment

Interactive · edit the input

implication graph: literal 1 above, ¬1 below · 6 vertices · 8 edges

¬1

¬2

¬3

Current literalOn the Tarjan stackComponent 1Component 2Component 3Conflict: x and ¬x together

clauses (a or b)

1 ∨ 2

¬1 ∨ 3

¬2 ∨ ¬3

¬1 ∨ ¬2

component of each literal

–1

–¬1

–2

–¬2

–3

–¬3

Tarjan stack (top on the right)

empty

Setup

Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.

Step 1 / 13

Java

1static int timer = 0, count = 0;
2static int[] tin, low, comp;
3static boolean[] onStack;
4static Deque<Integer> stack = new ArrayDeque<>();
5static void tarjan(List<Integer>[] g, int u) {        // numbers components in the order they finish (sinks first)
6    tin[u] = low[u] = ++timer;
7    stack.push(u); onStack[u] = true;
8    for (int v : g[u]) {
9        if (tin[v] == 0) { tarjan(g, v); low[u] = Math.min(low[u], low[v]); }
10        else if (onStack[v]) low[u] = Math.min(low[u], tin[v]);
11    }
12    if (low[u] == tin[u]) {                           // u is the root of a strongly connected component
13        int x;
14        do { x = stack.pop(); onStack[x] = false; comp[x] = count; } while (x != u);
15        count++;
16    }
17}
18static boolean[] solve2Sat(int n, int[][] clauses) {  // literal l: variable l / 2, negated when l is odd; {a, b} means (a or b)
19    List<Integer>[] g = new List[2 * n];
20    for (int i = 0; i < 2 * n; i++) g[i] = new ArrayList<>();
21    for (int[] c : clauses) {
22        g[c[0] ^ 1].add(c[1]);                        // if a is false, b must be true
23        g[c[1] ^ 1].add(c[0]);                        // if b is false, a must be true
24    }
25    tin = new int[2 * n]; low = new int[2 * n]; comp = new int[2 * n]; onStack = new boolean[2 * n];
26    for (int i = 0; i < 2 * n; i++) if (tin[i] == 0) tarjan(g, i);
27    boolean[] value = new boolean[n];
28    for (int i = 0; i < n; i++) {
29        if (comp[2 * i] == comp[2 * i + 1]) return null;   // x and not x imply each other: unsatisfiable
30        value[i] = comp[2 * i] < comp[2 * i + 1];          // the literal whose component finished first is later in topological order
31    }
32    return value;
33}

Live state

0 components8 implications

variables

clauses

No condition evaluated on this step

Execution trace (dry run table)Show 13 steps

Step	Line	State	What happens
1	L22	variables=3 clauses=4	Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.
2	L6	literal=1 tin=1	Tarjan enters literal 1 (tin = low = 1).
3	L6	literal=3 tin=2	Tarjan enters literal 3 (tin = low = 2).
4	L6	literal=¬2 tin=3	Tarjan enters literal ¬2 (tin = low = 3).
5	L12	literal=1 component=C1	low = tin at 1: pop a strongly connected component C1 = {¬2, 3, 1}. Components finish in reverse topological order, so C1 is a sink.
6	L6	literal=¬1 tin=4	Tarjan enters literal ¬1 (tin = low = 4).
7	L6	literal=2 tin=5	Tarjan enters literal 2 (tin = low = 5).
8	L6	literal=¬3 tin=6	Tarjan enters literal ¬3 (tin = low = 6).
9	L12	literal=¬1 component=C2	low = tin at ¬1: pop a strongly connected component C2 = {¬3, 2, ¬1}. Components finish in reverse topological order, so C1 is a sink.
10	L30	variable=1 x=true	Variable 1: components C1 (for 1) and C2 (for ¬1) differ. 1 has the smaller number (it is later in topological order), so x1 = true.
11	L30	variable=2 x=false	Variable 2: components C2 (for 2) and C1 (for ¬2) differ. ¬2 has the smaller number (it is later in topological order), so x2 = false.
12	L30	variable=3 x=true	Variable 3: components C1 (for 3) and C2 (for ¬3) differ. 3 has the smaller number (it is later in topological order), so x3 = true.
13	L32	return=satisfiable assignment=x1=T x2=F x3=T	Satisfiable. Assignment: x1 = true, x2 = false, x3 = true. Every clause has at least one true literal.

38.05.2

Variable/negation nodes

Give each variable two vertices: one for the variable being true and one for it being false. With variables numbered from 0, use literal 2*v for xv and 2*v + 1 for ¬xv. Then the negation of any literal l is simply l ^ 1: flipping the lowest bit swaps the two.

Input is often written DIMACS style, with 3 meaning x3 and -3 meaning ¬x3. Convert with v > 0 ? 2*(v-1) : 2*(-v-1) + 1. The animation uses the same style: clause 1,-2 is (x1 ∨ ¬x2), and the graph shows the positive literal of each variable above its negation.

A clause with a single literal (a) is written as (a ∨ a): it adds the arrow ¬a → a, which forces a to be true. The “A unit clause (x1 or x1) forces x1” preset uses it: x1 is true, which forces x2 and then x3.

Written	Meaning	Literal id (variables numbered from 1)	Negation
3	x3 is true	4	5
-3	x3 is false	5	4
1,-2	x1 or not x2	0 and 3	1 and 2

Java

1static int literal(int dimacs) {                         // 3 -> x3, -3 -> not x3; ids start at 0
2    return dimacs > 0 ? 2 * (dimacs - 1) : 2 * (-dimacs - 1) + 1;
3}
4
5static String literalName(int l) {
6    return (l % 2 == 1 ? "!x" : "x") + (l / 2 + 1);
7}

2-SAT: implication graph, SCCs and the assignment

Interactive · edit the input

implication graph: literal 1 above, ¬1 below · 6 vertices · 8 edges

¬1

¬2

¬3

Current literalOn the Tarjan stackComponent 1Component 2Component 3Conflict: x and ¬x together

clauses (a or b)

1 ∨ 2

¬1 ∨ 3

¬2 ∨ ¬3

¬1 ∨ ¬2

component of each literal

–1

–¬1

–2

–¬2

–3

–¬3

Tarjan stack (top on the right)

empty

Setup

Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.

Step 1 / 13

Java

1static int timer = 0, count = 0;
2static int[] tin, low, comp;
3static boolean[] onStack;
4static Deque<Integer> stack = new ArrayDeque<>();
5static void tarjan(List<Integer>[] g, int u) {        // numbers components in the order they finish (sinks first)
6    tin[u] = low[u] = ++timer;
7    stack.push(u); onStack[u] = true;
8    for (int v : g[u]) {
9        if (tin[v] == 0) { tarjan(g, v); low[u] = Math.min(low[u], low[v]); }
10        else if (onStack[v]) low[u] = Math.min(low[u], tin[v]);
11    }
12    if (low[u] == tin[u]) {                           // u is the root of a strongly connected component
13        int x;
14        do { x = stack.pop(); onStack[x] = false; comp[x] = count; } while (x != u);
15        count++;
16    }
17}
18static boolean[] solve2Sat(int n, int[][] clauses) {  // literal l: variable l / 2, negated when l is odd; {a, b} means (a or b)
19    List<Integer>[] g = new List[2 * n];
20    for (int i = 0; i < 2 * n; i++) g[i] = new ArrayList<>();
21    for (int[] c : clauses) {
22        g[c[0] ^ 1].add(c[1]);                        // if a is false, b must be true
23        g[c[1] ^ 1].add(c[0]);                        // if b is false, a must be true
24    }
25    tin = new int[2 * n]; low = new int[2 * n]; comp = new int[2 * n]; onStack = new boolean[2 * n];
26    for (int i = 0; i < 2 * n; i++) if (tin[i] == 0) tarjan(g, i);
27    boolean[] value = new boolean[n];
28    for (int i = 0; i < n; i++) {
29        if (comp[2 * i] == comp[2 * i + 1]) return null;   // x and not x imply each other: unsatisfiable
30        value[i] = comp[2 * i] < comp[2 * i + 1];          // the literal whose component finished first is later in topological order
31    }
32    return value;
33}

Live state

0 components8 implications

variables

clauses

No condition evaluated on this step

Execution trace (dry run table)Show 13 steps

Step	Line	State	What happens
1	L22	variables=3 clauses=4	Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.
2	L6	literal=1 tin=1	Tarjan enters literal 1 (tin = low = 1).
3	L6	literal=3 tin=2	Tarjan enters literal 3 (tin = low = 2).
4	L6	literal=¬2 tin=3	Tarjan enters literal ¬2 (tin = low = 3).
5	L12	literal=1 component=C1	low = tin at 1: pop a strongly connected component C1 = {¬2, 3, 1}. Components finish in reverse topological order, so C1 is a sink.
6	L6	literal=¬1 tin=4	Tarjan enters literal ¬1 (tin = low = 4).
7	L6	literal=2 tin=5	Tarjan enters literal 2 (tin = low = 5).
8	L6	literal=¬3 tin=6	Tarjan enters literal ¬3 (tin = low = 6).
9	L12	literal=¬1 component=C2	low = tin at ¬1: pop a strongly connected component C2 = {¬3, 2, ¬1}. Components finish in reverse topological order, so C1 is a sink.
10	L30	variable=1 x=true	Variable 1: components C1 (for 1) and C2 (for ¬1) differ. 1 has the smaller number (it is later in topological order), so x1 = true.
11	L30	variable=2 x=false	Variable 2: components C2 (for 2) and C1 (for ¬2) differ. ¬2 has the smaller number (it is later in topological order), so x2 = false.
12	L30	variable=3 x=true	Variable 3: components C1 (for 3) and C2 (for ¬3) differ. 3 has the smaller number (it is later in topological order), so x3 = true.
13	L32	return=satisfiable assignment=x1=T x2=F x3=T	Satisfiable. Assignment: x1 = true, x2 = false, x3 = true. Every clause has at least one true literal.

38.05.3

SCC unsatisfiable condition

If x and ¬x are in the same SCC, each can reach the other: x true forces ¬x true, and ¬x true forces x true. Neither value works, so the formula is **unsatisfiable**. The “Unsatisfiable: x1 is forced both ways” preset (1,2 1,-2 -1,2 -1,-2) puts all four literals in one component.

The converse is the surprising part: if **no** variable shares a component with its negation, the formula **is** satisfiable. The mirror symmetry of the implication graph guarantees it: each component has a mirror component made of the negated literals, and the assignment below picks consistently between mirrors. So the whole satisfiability question is “does any comp[2v] == comp[2v+1]?”.

This is a decision procedure in O(n + m): build the graph, run an SCC algorithm (Tarjan from the previous lesson), and scan the variables.

Java

1static boolean satisfiable(int n, int[][] clauses) {
2    int[] comp = tarjanScc(implicationGraph(n, clauses));
3    for (int v = 0; v < n; v++) if (comp[2 * v] == comp[2 * v + 1]) return false;   // x and not x imply each other
4    return true;
5}

Worst

O(n + m)

Space

O(n + m)

2-SAT: implication graph, SCCs and the assignment

Interactive · edit the input

implication graph: literal 1 above, ¬1 below · 6 vertices · 8 edges

¬1

¬2

¬3

Current literalOn the Tarjan stackComponent 1Component 2Component 3Conflict: x and ¬x together

clauses (a or b)

1 ∨ 2

¬1 ∨ 3

¬2 ∨ ¬3

¬1 ∨ ¬2

component of each literal

–1

–¬1

–2

–¬2

–3

–¬3

Tarjan stack (top on the right)

empty

Setup

Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.

Step 1 / 13

Java

1static int timer = 0, count = 0;
2static int[] tin, low, comp;
3static boolean[] onStack;
4static Deque<Integer> stack = new ArrayDeque<>();
5static void tarjan(List<Integer>[] g, int u) {        // numbers components in the order they finish (sinks first)
6    tin[u] = low[u] = ++timer;
7    stack.push(u); onStack[u] = true;
8    for (int v : g[u]) {
9        if (tin[v] == 0) { tarjan(g, v); low[u] = Math.min(low[u], low[v]); }
10        else if (onStack[v]) low[u] = Math.min(low[u], tin[v]);
11    }
12    if (low[u] == tin[u]) {                           // u is the root of a strongly connected component
13        int x;
14        do { x = stack.pop(); onStack[x] = false; comp[x] = count; } while (x != u);
15        count++;
16    }
17}
18static boolean[] solve2Sat(int n, int[][] clauses) {  // literal l: variable l / 2, negated when l is odd; {a, b} means (a or b)
19    List<Integer>[] g = new List[2 * n];
20    for (int i = 0; i < 2 * n; i++) g[i] = new ArrayList<>();
21    for (int[] c : clauses) {
22        g[c[0] ^ 1].add(c[1]);                        // if a is false, b must be true
23        g[c[1] ^ 1].add(c[0]);                        // if b is false, a must be true
24    }
25    tin = new int[2 * n]; low = new int[2 * n]; comp = new int[2 * n]; onStack = new boolean[2 * n];
26    for (int i = 0; i < 2 * n; i++) if (tin[i] == 0) tarjan(g, i);
27    boolean[] value = new boolean[n];
28    for (int i = 0; i < n; i++) {
29        if (comp[2 * i] == comp[2 * i + 1]) return null;   // x and not x imply each other: unsatisfiable
30        value[i] = comp[2 * i] < comp[2 * i + 1];          // the literal whose component finished first is later in topological order
31    }
32    return value;
33}

Live state

0 components8 implications

variables

clauses

No condition evaluated on this step

Execution trace (dry run table)Show 13 steps

Step	Line	State	What happens
1	L22	variables=3 clauses=4	Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.
2	L6	literal=1 tin=1	Tarjan enters literal 1 (tin = low = 1).
3	L6	literal=3 tin=2	Tarjan enters literal 3 (tin = low = 2).
4	L6	literal=¬2 tin=3	Tarjan enters literal ¬2 (tin = low = 3).
5	L12	literal=1 component=C1	low = tin at 1: pop a strongly connected component C1 = {¬2, 3, 1}. Components finish in reverse topological order, so C1 is a sink.
6	L6	literal=¬1 tin=4	Tarjan enters literal ¬1 (tin = low = 4).
7	L6	literal=2 tin=5	Tarjan enters literal 2 (tin = low = 5).
8	L6	literal=¬3 tin=6	Tarjan enters literal ¬3 (tin = low = 6).
9	L12	literal=¬1 component=C2	low = tin at ¬1: pop a strongly connected component C2 = {¬3, 2, ¬1}. Components finish in reverse topological order, so C1 is a sink.
10	L30	variable=1 x=true	Variable 1: components C1 (for 1) and C2 (for ¬1) differ. 1 has the smaller number (it is later in topological order), so x1 = true.
11	L30	variable=2 x=false	Variable 2: components C2 (for 2) and C1 (for ¬2) differ. ¬2 has the smaller number (it is later in topological order), so x2 = false.
12	L30	variable=3 x=true	Variable 3: components C1 (for 3) and C2 (for ¬3) differ. 3 has the smaller number (it is later in topological order), so x3 = true.
13	L32	return=satisfiable assignment=x1=T x2=F x3=T	Satisfiable. Assignment: x1 = true, x2 = false, x3 = true. Every clause has at least one true literal.

38.05.4

Assignment construction

To build an assignment, use the component order. Tarjan numbers components in reverse topological order, so a literal in a **lower-numbered** component is later in topological order. Set xv true exactly when comp[xv] < comp[¬xv]: pick the literal that comes later, because nothing reachable from it can contradict it.

On the “Satisfiable” preset the literal components are 1: C1, ¬1: C2, 2: C2, ¬2: C1, 3: C1, ¬3: C2. That yields x1 = true, x2 = false, x3 = true. Check the four clauses: 1 ∨ 2 is true through x1; ¬1 ∨ 3 through x3; ¬2 ∨ ¬3 through ¬x2; ¬1 ∨ ¬2 through ¬x2.

Another valid assignment may exist; this procedure returns one. If every clause must hold, finding all solutions is a counting problem and is much harder.

Java

1static boolean[] solve2Sat(int n, int[][] clauses) {     // null when unsatisfiable
2    int[] comp = tarjanScc(implicationGraph(n, clauses));
3    boolean[] value = new boolean[n];
4    for (int v = 0; v < n; v++) {
5        if (comp[2 * v] == comp[2 * v + 1]) return null;
6        value[v] = comp[2 * v] < comp[2 * v + 1];        // the literal whose component finishes first is later in topological order
7    }
8    return value;
9}

2-SAT: implication graph, SCCs and the assignment

Interactive · edit the input

implication graph: literal 1 above, ¬1 below · 6 vertices · 8 edges

¬1

¬2

¬3

Current literalOn the Tarjan stackComponent 1Component 2Component 3Conflict: x and ¬x together

clauses (a or b)

1 ∨ 2

¬1 ∨ 3

¬2 ∨ ¬3

¬1 ∨ ¬2

component of each literal

–1

–¬1

–2

–¬2

–3

–¬3

Tarjan stack (top on the right)

empty

Setup

Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.

Step 1 / 13

Java

1static int timer = 0, count = 0;
2static int[] tin, low, comp;
3static boolean[] onStack;
4static Deque<Integer> stack = new ArrayDeque<>();
5static void tarjan(List<Integer>[] g, int u) {        // numbers components in the order they finish (sinks first)
6    tin[u] = low[u] = ++timer;
7    stack.push(u); onStack[u] = true;
8    for (int v : g[u]) {
9        if (tin[v] == 0) { tarjan(g, v); low[u] = Math.min(low[u], low[v]); }
10        else if (onStack[v]) low[u] = Math.min(low[u], tin[v]);
11    }
12    if (low[u] == tin[u]) {                           // u is the root of a strongly connected component
13        int x;
14        do { x = stack.pop(); onStack[x] = false; comp[x] = count; } while (x != u);
15        count++;
16    }
17}
18static boolean[] solve2Sat(int n, int[][] clauses) {  // literal l: variable l / 2, negated when l is odd; {a, b} means (a or b)
19    List<Integer>[] g = new List[2 * n];
20    for (int i = 0; i < 2 * n; i++) g[i] = new ArrayList<>();
21    for (int[] c : clauses) {
22        g[c[0] ^ 1].add(c[1]);                        // if a is false, b must be true
23        g[c[1] ^ 1].add(c[0]);                        // if b is false, a must be true
24    }
25    tin = new int[2 * n]; low = new int[2 * n]; comp = new int[2 * n]; onStack = new boolean[2 * n];
26    for (int i = 0; i < 2 * n; i++) if (tin[i] == 0) tarjan(g, i);
27    boolean[] value = new boolean[n];
28    for (int i = 0; i < n; i++) {
29        if (comp[2 * i] == comp[2 * i + 1]) return null;   // x and not x imply each other: unsatisfiable
30        value[i] = comp[2 * i] < comp[2 * i + 1];          // the literal whose component finished first is later in topological order
31    }
32    return value;
33}

Live state

0 components8 implications

variables

clauses

No condition evaluated on this step

Execution trace (dry run table)Show 13 steps

Step	Line	State	What happens
1	L22	variables=3 clauses=4	Each clause (a ∨ b) gives two implications: ¬a → b and ¬b → a. 3 variables give 6 literal vertices and 4 clauses give 8 arrows.
2	L6	literal=1 tin=1	Tarjan enters literal 1 (tin = low = 1).
3	L6	literal=3 tin=2	Tarjan enters literal 3 (tin = low = 2).
4	L6	literal=¬2 tin=3	Tarjan enters literal ¬2 (tin = low = 3).
5	L12	literal=1 component=C1	low = tin at 1: pop a strongly connected component C1 = {¬2, 3, 1}. Components finish in reverse topological order, so C1 is a sink.
6	L6	literal=¬1 tin=4	Tarjan enters literal ¬1 (tin = low = 4).
7	L6	literal=2 tin=5	Tarjan enters literal 2 (tin = low = 5).
8	L6	literal=¬3 tin=6	Tarjan enters literal ¬3 (tin = low = 6).
9	L12	literal=¬1 component=C2	low = tin at ¬1: pop a strongly connected component C2 = {¬3, 2, ¬1}. Components finish in reverse topological order, so C1 is a sink.
10	L30	variable=1 x=true	Variable 1: components C1 (for 1) and C2 (for ¬1) differ. 1 has the smaller number (it is later in topological order), so x1 = true.
11	L30	variable=2 x=false	Variable 2: components C2 (for 2) and C1 (for ¬2) differ. ¬2 has the smaller number (it is later in topological order), so x2 = false.
12	L30	variable=3 x=true	Variable 3: components C1 (for 3) and C2 (for ¬3) differ. 3 has the smaller number (it is later in topological order), so x3 = true.
13	L32	return=satisfiable assignment=x1=T x2=F x3=T	Satisfiable. Assignment: x1 = true, x2 = false, x3 = true. Every clause has at least one true literal.

Practice ladder

Now try it yourself

Easy

Find the Town Judge

Medium

Possible Bipartition
Is Graph Bipartite?
Satisfiability of Equality Equations

Advanced

Couples Holding Hands
Maximum Employees to Be Invited to a Meeting

Key takeaways

Each clause (a or b) gives not-a implies b and not-b implies a.
Unsatisfiable exactly when some variable and its negation share an SCC.
Otherwise set x true when its component number is smaller than the negation's (Tarjan numbering).