02
SAT Problem
Chapter 2 • Advanced
120 min
SAT Problem
Boolean Satisfiability (SAT)
Given a Boolean formula, is there an assignment making it true?
3-SAT
Each clause has exactly 3 literals.
Example
(x₁ ∨ ¬x₂ ∨ x₃) ∧ (¬x₁ ∨ x₂ ∨ x₄) ∧ (x₂ ∨ ¬x₃ ∨ ¬x₄)
Cook-Levin Theorem
SAT is NP-Complete
First problem proven NP-complete.
2-SAT
Polynomial-time solvable using strongly connected components.
python.js
def solve_2sat(clauses, n):
"""
Solve 2-SAT using SCC.
clauses: [(x1, x2), ...] where x can be negative
"""
# Build implication graph
graph = [[] for _ in range(2 * n)]
for a, b in clauses:
# a ∨ b = ¬a → b and ¬b → a
graph[negate(a, n)].append(b)
graph[negate(b, n)].append(a)
# Find SCCs
sccs = find_sccs(graph)
# Check if x and ¬x in same SCC
for i in range(n):
if sccs[i] == sccs[i + n]:
return None # Unsatisfiable
return True # Satisfiable
Practice Problems
- Reduce 3-SAT to Independent Set
- Solve 2-SAT
- MAX-SAT approximation