ADVANCED ALGORITHMS - NP-COMPLETENESS:SAT, 3-SAT and the Cook-Levin Theorem

SAT, 3-SAT and the Cook-Levin Theorem

Boolean Satisfiability (SAT)

SAT: Given a Boolean formula φ over variables x₁, …, xₙ, is there a truth assignment making φ true?

CNF-SAT: φ is in Conjunctive Normal Form — a conjunction of clauses, each clause being a disjunction of literals.

Example: (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₃) ∧ (x₂ ∨ ¬x₃)

The Cook-Levin Theorem (1971–1972)

Theorem: SAT is NP-complete.

This was the first problem proven NP-complete. Stephen Cook (1971) and Leonid Levin (independently, 1972) showed that every problem in NP reduces to SAT.

Proof sketch (SAT is NP-hard):

For any problem L ∈ NP, there is a polynomial-time verifier V(x, c). We encode the computation of V as a SAT formula:

• Variables for each cell of V's computation tableau at each time step
• Clauses enforcing the transition rules of V's computation
• Resulting formula is satisfiable ↔ V accepts ↔ x ∈ L

3-SAT

3-SAT: Every clause has exactly 3 literals.

(x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ x₂ ∨ x₄) ∧ (x₂ ∨ ¬x₃ ∨ ¬x₄)

3-SAT is NP-complete (proven by reduction from SAT):

• Split large clauses into 3-literal clauses using auxiliary variables
• A clause (l₁ ∨ l₂ ∨ l₃ ∨ l₄) becomes (l₁ ∨ l₂ ∨ y) ∧ (¬y ∨ l₃ ∨ l₄)

2-SAT is in P

When clauses have exactly 2 literals, we can solve it in linear time using strongly connected components (SCC):

Key insight: Clause (a ∨ b) ≡ (¬a → b) ∧ (¬b → a)

Build an implication graph:

• 2n nodes: one for each variable and its negation
• For each clause (a ∨ b): add edges ¬a → b and ¬b → a

2-SAT is unsatisfiable ↔ some variable xᵢ and ¬xᵢ are in the same SCC.

from collections import defaultdict

def solve_2sat(n, clauses):
    """
    Solve 2-SAT in O(V + E) using Kosaraju's SCC algorithm.
    n: number of variables (1-indexed)
    clauses: list of (a, b) where negative means negation
    Returns: assignment list or None if unsatisfiable
    """
    # Node 2i = xᵢ (positive), node 2i+1 = ¬xᵢ (negative)
    def pos(x): return 2 * (x - 1)
    def neg(x): return 2 * (x - 1) + 1
    def negate_lit(lit): return lit ^ 1  # flip last bit

    graph = defaultdict(list)
    rev_graph = defaultdict(list)
    
    for a, b in clauses:
        u = pos(a) if a > 0 else neg(-a)
        v = pos(b) if b > 0 else neg(-b)
        na = negate_lit(u)
        nb = negate_lit(v)
        # Clause (a ∨ b) → implication ¬a → b and ¬b → a
        graph[na].append(v)
        graph[nb].append(u)
        rev_graph[v].append(na)
        rev_graph[u].append(nb)
    
    # Kosaraju's algorithm
    visited = [False] * (2 * n)
    order = []
    
    def dfs1(v):
        visited[v] = True
        for u in graph[v]:
            if not visited[u]:
                dfs1(u)
        order.append(v)
    
    for v in range(2 * n):
        if not visited[v]:
            dfs1(v)
    
    comp = [-1] * (2 * n)
    c = 0
    
    def dfs2(v, c):
        comp[v] = c
        for u in rev_graph[v]:
            if comp[u] == -1:
                dfs2(u, c)
    
    for v in reversed(order):
        if comp[v] == -1:
            dfs2(v, c)
            c += 1
    
    assignment = []
    for i in range(1, n + 1):
        if comp[pos(i)] == comp[neg(i)]:
            return None  # Unsatisfiable
        # Assign True if positive literal has higher comp number (later in topological order)
        assignment.append(comp[pos(i)] > comp[neg(i)])
    
    return assignment

# Example: (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3)
result = solve_2sat(3, [(1, 2), (-1, 3), (-2, -3)])
print(result)  # e.g. [False, True, True]

Variants and Complexity

Practical Implications

Recognizing that a problem encodes SAT is a powerful skill:

• Constraint satisfaction problems (Sudoku, N-queens) are often SAT instances
• Register allocation in compilers reduces to graph coloring, which reduces to 3-SAT
• Circuit design verification is SAT
• Modern SAT solvers (DPLL, CDCL) handle millions of variables in practice despite worst-case NP

Practice Problems

1. Reduce 3-SAT to Independent Set (classic)
2. Solve 2-SAT: given clauses (¬x ∨ y), (¬y ∨ z), (¬z ∨ x), (x ∨ y)
3. Implement the 2-SAT implication graph and find satisfying assignment
4. Prove MAX-2-SAT is NP-hard via reduction from 3-SAT