Mathematics.

logic and complexity

Propositional Satisfiability (SAT)

Discrete Mathematics25 minDifficulty5 out of 10

You should know: propositional logic, boolean algebra

Overview

The Boolean satisfiability problem (SAT) asks, given a propositional logic formula built from variables, ∧, ∨, and ¬, whether there is some assignment of true/false to the variables that makes the whole formula evaluate to true. A formula that has such an assignment is satisfiable; one that has none (it is false under every assignment) is unsatisfiable, i.e. a contradiction. SAT is the canonical NP-complete problem: the Cook–Levin theorem (1971) proved that SAT is NP-complete, meaning every problem in NP can be reduced to it in polynomial time, and no known algorithm solves SAT in the worst case faster than roughly checking all 2ⁿ assignments (though practical SAT solvers using techniques like DPLL and conflict-driven clause learning routinely solve huge industrial instances). SAT is almost always studied in conjunctive normal form (CNF): a conjunction (AND) of clauses, each clause a disjunction (OR) of literals (variables or their negations), because any propositional formula can be converted to an equisatisfiable CNF formula.

Intuition

Think of each clause as a constraint that must be satisfied: (x ∨ y) says 'at least one of x, y must be true.' Satisfying a whole CNF formula means finding one assignment that keeps every constraint happy simultaneously — like a giant Sudoku where each clause is a small rule and you need a single grid filling that obeys all of them at once. The brute-force approach tries all 2ⁿ assignments, which is why SAT is believed to require exponential time in the worst case (this is exactly the P vs NP question — a fast SAT algorithm would imply P = NP). But structure helps enormously in practice: if a clause has only one literal left after other variables are fixed, that literal's value is forced (unit propagation), and this alone lets modern solvers prune the search tree by orders of magnitude, which is why SAT solvers can handle formulas with millions of variables arising from hardware verification and scheduling.

Formal Definition

Definition

A CNF formula over variables x₁,…,xₙ is a conjunction of clauses Cⱼ, each a disjunction of literals. A satisfying assignment is a function v: {x₁,…,xₙ} → {0,1} making the formula true:

φ=C1∧C2∧⋯∧Cm,Cj=ℓj,1∨ℓj,2∨⋯\varphi = C_1 \land C_2 \land \cdots \land C_m, \qquad C_j = \ell_{j,1} \lor \ell_{j,2} \lor \cdots
Conjunctive normal form (CNF)
SAT(φ)=∃ v:{x1,…,xn}→{0,1} such that φ(v)=1\text{SAT}(\varphi) = \exists\, v : \{x_1,\ldots,x_n\} \to \{0,1\} \text{ such that } \varphi(v) = 1
Satisfiability
2-SAT: every clause has≤2 literals  ⟹  solvable in O(n+m)\text{2-SAT: every clause has} \le 2 \text{ literals} \implies \text{solvable in } O(n+m)
2-SAT is in P
3-SAT: every clause has exactly 3 literals  ⟹  NP-complete\text{3-SAT: every clause has exactly 3 literals} \implies \text{NP-complete}
3-SAT (Cook–Levin, 1971)

Worked Examples

  1. Try x = true, y = false, z = true. Evaluate the first clause.

    (x∨y)=(T∨F)=T(x \lor y) = (T \lor F) = T

  2. Evaluate the second clause with the same assignment.

    (¬x∨z)=(F∨T)=T(\lnot x \lor z) = (F \lor T) = T

  3. Both clauses are true, so the conjunction is true.

    φ=T∧T=T\varphi = T \land T = T

Answer: Satisfiable: x = true, y = false, z = true is one satisfying assignment.

Practice Problems

Difficulty 3/10

Evaluate φ = (x ∨ ¬y) ∧ (y ∨ z) at x = false, y = true, z = false. Is φ true or false under this assignment?

Difficulty 4/10

Determine whether φ = (x1 ∨ x2) ∧ (¬x1 ∨ x2) ∧ (x1 ∨ ¬x2) is satisfiable by testing all 4 assignments of (x1, x2).

Difficulty 6/10

A scheduler must assign each of two tasks A, B to true (run on machine 1) or false (run on machine 2), subject to the constraint clause (A ∨ B) (at least one task on machine 1) and (¬A ∨ ¬B) (not both tasks on machine 1, since that would overload it). List all valid schedules.

Quiz

A propositional formula is 'satisfiable' if:
The Cook–Levin theorem established that:
Unlike general SAT and 3-SAT, 2-SAT (every clause has at most 2 literals) is:

Summary

  • SAT asks whether a propositional formula has some assignment of truth values making it true (satisfiable) or none (unsatisfiable).
  • SAT is almost always posed in CNF: a conjunction of clauses, each a disjunction of literals.
  • The Cook–Levin theorem (1971) proved SAT is NP-complete — the first problem shown to be so, anchoring the theory of NP-completeness.
  • 2-SAT is solvable in polynomial time, but 3-SAT (and general SAT) is NP-complete — the boundary between P and NP-hard passes right between clause lengths 2 and 3.
  • Practical SAT solvers (DPLL, CDCL) exploit structure like unit propagation to solve huge real-world instances despite the worst-case exponential bound.

References

  1. WebsiteWikipedia — Boolean satisfiability problem
  2. WebsiteWikipedia — Cook–Levin theorem