Prerequisite:

Boolean satisfiability is where theory meets practice in the most dramatic way possible. SAT solvers that handle millions of variables now underpin hardware verification, software analysis, and AI planning - and the theoretical story of why SAT is hard, and when it is not, is one of the most beautiful in all of computer science.

The SAT Problem

A Boolean formula in Conjunctive Normal Form (CNF) is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals. A literal is a variable $x_i$ or its negation $\neg x_i$.

Definition. The SAT problem: given a CNF formula $\varphi$ over variables $x_1, \ldots, x_n$, does there exist a truth assignment $\alpha : {x_1, \ldots, x_n} \to {0, 1}$ such that $\varphi(\alpha) = 1$?

For example, the formula

$$\varphi = (x_1 \vee \neg x_2) \wedge (\neg x_1 \vee x_3) \wedge (x_2 \vee \neg x_3)$$

is satisfied by $x_1 = 1, x_2 = 1, x_3 = 1$. The clause structure is what gives CNF its power: each clause rules out at least one assignment, and satisfying $\varphi$ means surviving all the constraints simultaneously.

The Cook-Levin Theorem: 3-SAT is NP-Complete

Theorem (Cook 1971, Levin 1973). SAT is NP-complete. Consequently, 3-SAT - SAT restricted to clauses of size exactly 3 - is also NP-complete.

The proof proceeds by reducing every language in NP to SAT. Given a nondeterministic Turing machine $M$ that decides a language $L$ in polynomial time, and an input $x$, we encode the entire computation tableau of $M$ on $x$ as a CNF formula. Variables encode the state, head position, and tape contents at each time step. Four groups of clauses enforce:

  1. The initial configuration matches $x$.
  2. Transitions are valid according to $M$’s transition function.
  3. The machine reaches an accepting state.
  4. Each cell/state is consistent (exactly one value at each position/time pair).

The resulting formula has size polynomial in $|x|$ and is satisfiable if and only if $M$ accepts $x$. This is the founding result of NP-completeness theory.

2-SAT is in P

Restricting clauses to at most 2 literals gives 2-SAT, which is solvable in linear time via an elegant graph-based approach.

Key insight. Every 2-clause $(a \vee b)$ is logically equivalent to two implications: $\neg a \Rightarrow b$ and $\neg b \Rightarrow a$.

Algorithm (Implication Graph + Kosaraju SCC).

  1. Build an implication graph $G$ with $2n$ nodes: one for each literal $x_i$ and $\neg x_i$.
  2. For each clause $(a \vee b)$, add directed edges $\neg a \to b$ and $\neg b \to a$.
  3. Compute strongly connected components (SCCs) of $G$ using Kosaraju’s or Tarjan’s algorithm in $O(V + E)$.
  4. The formula is unsatisfiable if and only if some variable $x_i$ and its negation $\neg x_i$ appear in the same SCC.
  5. If satisfiable, assign values: for each variable, assign $x_i = 1$ if $x_i$’s SCC has a higher topological order than $\neg x_i$’s SCC, and $x_i = 0$ otherwise.

Proof of correctness. If $x_i$ and $\neg x_i$ are in the same SCC, then $x_i \Rightarrow^\ast \neg x_i$ and $\neg x_i \Rightarrow^\ast x_i$, meaning both must hold simultaneously - a contradiction. Conversely, if they are in different SCCs, the topological assignment is consistent by transitivity of implication.

This gives a complete polynomial-time algorithm. The jump from 2-SAT (in P) to 3-SAT (NP-complete) represents one of the sharpest dichotomies in complexity theory.

Modern SAT Solvers: DPLL and CDCL

For 3-SAT and beyond, exact solvers use exponential-time algorithms in the worst case, but perform remarkably well on structured industrial instances.

The DPLL Algorithm (Davis-Putnam-Logemann-Loveland, 1962) is a backtracking search with two key propagation rules:

  • Unit propagation. If a clause contains exactly one unset literal, that literal must be set to true. This forces assignments and can trigger cascading propagations.
  • Pure literal elimination. If a literal appears only positively (or only negatively) across all remaining clauses, set it to satisfy all such clauses.

DPLL selects an unset variable, branches on its value, propagates, and backtracks upon conflict.

Conflict-Driven Clause Learning (CDCL) is the breakthrough that made industrial SAT solving practical. When DPLL discovers a contradiction, it does not simply undo the last choice. Instead:

  1. Conflict analysis. Build the implication graph of the current decision level, tracing which assignments forced the conflict. Find the Unique Implication Point (UIP) - the last single node that dominates all paths to the conflict.
  2. Clause learning. Extract a new clause from the cut at the UIP. This learned clause is a logical consequence of the formula and will prevent the solver from making the same mistake in future branches.
  3. Non-chronological backjumping. Rather than undoing only the most recent decision, jump back to the second-highest decision level among the literals in the learned clause - the earliest point at which the clause becomes unit propagating.

Learned clauses accumulate and prune the search space globally, giving CDCL super-polynomial speedups over pure DPLL on structured problems.

Variable Ordering: VSIDS. The Variable State Independent Decaying Sum heuristic assigns each variable an activity score, incrementing it each time the variable appears in a conflict clause. Scores decay periodically (multiply by a constant $< 1$). The highest-activity variable is chosen next. This focuses search on recently-conflicting variables, which tend to be the most constrained.

Restart Strategies. Modern solvers periodically restart the search from scratch, retaining all learned clauses. Restarts prevent the solver from getting trapped in unproductive regions of the search tree, and the interaction between restarts and learned clauses is a major driver of solver performance.

MAX-SAT

Definition. Given a CNF formula $\varphi$ with $m$ clauses, MAX-SAT asks for an assignment maximising the number of satisfied clauses.

MAX-SAT is NP-hard. A simple randomised argument shows that setting each variable independently and uniformly at random satisfies each $k$-clause independently with probability $1 - 2^{-k}$, giving an expected $(1 - 2^{-k})$-approximation for $k$-MAX-SAT. For 3-MAX-SAT this is $7/8$, and the Hastad inapproximability theorem shows that $7/8 + \varepsilon$ is NP-hard to achieve for any $\varepsilon > 0$, assuming $P \neq NP$.

Satisfiability Modulo Theories (SMT)

Real-world verification problems involve arithmetic, arrays, and data structures - not just Boolean variables. SMT solvers extend SAT with theory solvers for specific domains.

Architecture (DPLL(T)).

  • A SAT solver handles the Boolean skeleton of the formula.
  • Theory solvers handle fragments: linear arithmetic ($\mathcal{T}{LIA}$), real arithmetic ($\mathcal{T}{LRA}$), uninterpreted functions ($\mathcal{T}{EUF}$), arrays ($\mathcal{T}{ARR}$), bit-vectors ($\mathcal{T}_{BV}$).
  • The SAT solver finds a Boolean satisfying assignment; the theory solver checks if the corresponding conjunction of theory literals is consistent. If not, it generates a theory conflict clause that the SAT solver learns and uses to prune future search.

This tight integration makes SMT solvers far more expressive than pure SAT, while retaining the efficiency of CDCL for the Boolean backbone.

Examples

Hardware verification. Checking that a circuit satisfies a specification is encoded as SAT: model the circuit’s gate logic as CNF, add the negation of the desired property, and ask whether the result is satisfiable. A satisfying assignment is a counterexample; unsatisfiability proves correctness.

Scheduling as SAT. Assign jobs to time slots subject to capacity and precedence constraints. Introduce variables $y_{j,t}$ (“job $j$ runs in slot $t$") and encode constraints as clauses. An industrial job-shop scheduling instance with thousands of jobs maps naturally to a CNF formula that SAT solvers can handle.

Sudoku as SAT. A 9x9 Sudoku puzzle encodes directly as 3-SAT. Variables $x_{r,c,v}$ represent “cell $(r,c)$ has value $v$.” Row, column, box, and uniqueness constraints each contribute O(1) clauses per cell. Modern SAT solvers solve any puzzle instance in milliseconds.

Formal software verification. Tools like Microsoft’s Z3 and Stanford’s CVC5 use SMT to verify loop invariants, check buffer overflow conditions, and synthesise correct programs from specifications. A developer-written assertion is negated and passed to the SMT solver; a satisfying assignment is a concrete bug-triggering input.

Read Next: