SAT solving

SAT solving begins with a Boolean formula whose variables take the values true or false. The task is to find a satisfying assignment, or to establish that every assignment violates at least one constraint.¹ A common input form is conjunctive normal form (CNF), a conjunction of clauses, each clause being a disjunction of literals such as x or not x. For example, (x or y) and (not x or z) is satisfied by any assignment meeting both clauses.

The general satisfiability problem was shown to be NP-complete by the Cook–Levin theorem, making it a central subject in computational complexity theory.¹ Hardness in the worst case does not mean every practical instance is difficult: industrial formulas often contain structure that solvers can exploit.

Modern SAT solvers combine systematic search with deductions that reduce the remaining search space. The classical DPLL procedure repeatedly chooses a variable, assigns a value, and propagates consequences; if a contradiction appears, it backtracks and tries another branch.³ Unit propagation is especially important: a clause with all but one literal false forces its remaining literal to true.

Conflict-driven clause learning (CDCL) extends this process by analyzing contradictions and recording a new clause that prevents the same combination of decisions from recurring.² Solvers also use non-chronological backtracking, variable-activity scores, phase selection, clause deletion, and restarts. These mechanisms are heuristic, but the underlying deductions preserve correctness; a reported satisfying assignment can be checked directly, while an unsatisfiability proof can be independently verified.

SAT solving is often used as a back end for problems that are not initially written as Boolean formulas. A finite-domain constraint, circuit, planning rule, or software property can be translated into variables and clauses; the solver then searches for a model of the encoding.³ In hardware verification, SAT checks whether a circuit can reach an unwanted state or whether two designs differ. In software analysis, bounded model checking converts executions up to a selected length into SAT instances.

Other applications include scheduling, configuration, test generation, cryptographic analysis, automated planning, and formal verification. Encoding quality matters: two logically equivalent translations may differ greatly in clause count, propagation strength, and symmetry. Incremental SAT allows related formulas to be solved while retaining learned information, which is useful when constraints are added or removed across a sequence of queries.

SAT solving is shaped as much by benchmark structure and proof technology as by raw processor speed. The annual SAT Competition evaluates solvers on categories including crafted, random, and application instances, encouraging reproducible comparisons across changing workloads.⁴ A solver may excel on industrial formulas yet perform poorly on deliberately constructed instances.

Unsatisfiability is not merely the absence of a found model: modern proof-producing solvers can emit checkable resolution-style certificates, allowing a separate verifier to validate the result. Related extensions include quantified Boolean formula solving, which adds alternating existential and universal choices, and pseudo-Boolean solving, which represents weighted linear inequalities. SAT techniques also underlie SMT solvers, where Boolean search coordinates theories such as arithmetic or arrays rather than handling all constraints as ordinary clauses.⁵

Boolean satisfiability problem

The problem of deciding whether a Boolean formula has an assignment that makes it true.

CNF

Conjunctive normal form: a conjunction of clauses, with each clause formed from disjoined literals.

Unit propagation

The deduction that assigns the only remaining possible literal in a clause whose other literals are false.

CDCL

Conflict-driven clause learning, a DPLL-based method that analyzes conflicts and records learned clauses.

Incremental SAT

A solving mode that reuses a solver state and learned information across related formulas.