Algorithm for 2-Satisfiability problem

2-SAT

computational complexity

algorithms

satisfiability problem

graph theory

Algorithm for 2-Satisfiability problem

Master System Design with Codemia

Enhance your system design skills with over 120 practice problems, detailed solutions, and hands-on exercises.

Start Practicing Learn More

The 2-SAT problem asks whether a CNF formula with exactly two literals per clause is satisfiable.

Example clause: $(x_1 \lor \neg x_2)$ .

Unlike 3-SAT, 2-SAT is solvable in linear time using strongly connected components (SCCs).

Core Idea: Implication Graph

For each variable x, create two nodes:

x
~x

For each clause $(a \lor b)$ , add implications:

$(\neg a \to b)$
$(\neg b \to a)$

After building the graph, compute SCCs.

Satisfiability Condition

The formula is satisfiable iff for every variable x, nodes x and ~x are in different SCCs.

If any variable and its negation fall in the same SCC, the formula is unsatisfiable.

Getting an Assignment

After SCC computation (Kosaraju or Tarjan), assign truth values by SCC topological order:

process SCCs in reverse topological order,
set a literal true if its SCC appears after its negation SCC.

Python Reference Implementation

python

1def two_sat(num_vars, clauses):
2    # Variables are 1..num_vars. Literal encoding:
3    #  i  -> variable i
4    # -i  -> negation of variable i
5
6    def idx(lit):
7        v = abs(lit) - 1
8        return 2 * v + (0 if lit > 0 else 1)
9
10    def neg(i):
11        return i ^ 1
12
13    n = 2 * num_vars
14    g = [[] for _ in range(n)]
15    rg = [[] for _ in range(n)]
16
17    def add_edge(u, v):
18        g[u].append(v)
19        rg[v].append(u)
20
21    for a, b in clauses:
22        ai, bi = idx(a), idx(b)
23        add_edge(neg(ai), bi)
24        add_edge(neg(bi), ai)
25
26    order = []
27    seen = [False] * n
28
29    def dfs1(u):
30        seen[u] = True
31        for v in g[u]:
32            if not seen[v]:
33                dfs1(v)
34        order.append(u)
35
36    for i in range(n):
37        if not seen[i]:
38            dfs1(i)
39
40    comp = [-1] * n
41
42    def dfs2(u, c):
43        comp[u] = c
44        for v in rg[u]:
45            if comp[v] == -1:
46                dfs2(v, c)
47
48    c = 0
49    for u in reversed(order):
50        if comp[u] == -1:
51            dfs2(u, c)
52            c += 1
53
54    assignment = [False] * (num_vars + 1)
55    for var in range(1, num_vars + 1):
56        t = idx(var)
57        f = idx(-var)
58        if comp[t] == comp[f]:
59            return False, None
60        assignment[var] = comp[t] > comp[f]
61
62    return True, assignment[1:]
63
64
65ok, values = two_sat(
66    3,
67    [
68        (1, -2),   # (x1 v ~x2)
69        (-1, 3),   # (~x1 v x3)
70        (2, -3),   # (x2 v ~x3)
71    ],
72)
73print(ok, values)

Complexity

Let n be variables and m clauses:

Vertices: 2n
Edges: 2m
Time: O(n + m)
Space: O(n + m)

Summary

Topic	Result
Solver model	Implication graph + SCC
Unsat check	`x` and `~x` in same SCC
Complexity	Linear in graph size