SAT

The Boolean satisfiability problem, usually called SAT, is the problem of deciding whether a propositional formula has a satisfying assignment: a choice of true or false for each variable that makes the whole formula true^[3]. A formula with a satisfying assignment is satisfiable; one without is unsatisfiable, and its negation is a tautology. SAT was the first problem proved NP-complete, by Stephen Cook in 1971 and independently by Leonid Levin^[1][2]: any problem whose solutions can be checked in polynomial time can be translated into SAT in polynomial time. No algorithm is known that solves every instance in less than exponential time. Yet programs called SAT solvers, which search for an assignment and learn from their failures, routinely settle formulas from industry with millions of variables and clauses^[6][7][8]. Because so many problems can be encoded as satisfiability, a good SAT solver serves as a general-purpose engine for verification, planning, scheduling and combinatorial mathematics.

A propositional formula is built from Boolean variables with negation, conjunction and disjunction. SAT solvers take their input in conjunctive normal form (CNF): a conjunction of clauses, each a disjunction of literals, each a variable or its negation. For example,

is satisfied by setting $x_1$, $x_2$ and $x_3$ all false. CNF is no restriction: the Tseitin transformation converts any formula into a CNF formula that is satisfiable exactly when the original is, with only linear growth. The form suits solvers because the two facts that drive the search are immediate in it: a clause whose literals are all false is a conflict, and a clause with all literals but one false forces the remaining one, which is unit propagation. Instances are exchanged in the DIMACS text format.

Restrictions of SAT are named by the clause length: in $k$-SAT every clause has at most $k$ literals. 2-SAT can be solved in linear time^[18], as can Horn-SAT, where each clause has at most one positive literal, while 3-SAT is already NP-complete. Schaefer's dichotomy theorem of 1978 classified all such restrictions defined by the allowed kinds of constraint: each is either in P or NP-complete^[11].

SAT is in NP because a satisfying assignment, once guessed, can be checked in linear time. The Cook–Levin theorem shows that it is also NP-hard: the computation of a nondeterministic Turing machine on an input, for a polynomial number of steps, can be described by a polynomial-size formula whose satisfying assignments are exactly the accepting computations^[1][2]. Karp showed in 1972 that 21 classical combinatorial problems are NP-complete by reductions starting from SAT^[19], and thousands more have followed. A polynomial-time algorithm for SAT would therefore give one for every problem in NP, and it is widely believed that none exists. The exponential time hypothesis states the stronger conjecture that 3-SAT needs time $2^{\Omega (n)}$ for $n$ variables.

For unsatisfiable formulas, no short certificate is known either: whether every unsatisfiable formula has a proof of unsatisfiability of polynomial size is the question of whether NP equals co-NP. For the proof systems that solvers use, the answer is known to be no; the pigeonhole formulas have only exponentially long resolution refutations.

Complete solvers, which can prove unsatisfiability, descend from the procedure of Davis, Putnam, Logemann and Loveland, DPLL, of 1962: assign a variable, propagate the consequences, and backtrack on a conflict^[5]. Its successor, conflict-driven clause learning (CDCL), analyzes each conflict to learn a new clause that prevents it from recurring and jumps back over irrelevant decisions^[6]. Engineering made CDCL fast: watched literals for propagation, the VSIDS branching heuristic, restarts and clause deletion^[7][8]. Incomplete solvers based on local search, such as WalkSAT, start from a random assignment and repeatedly flip variables in unsatisfied clauses; they can find assignments for some large satisfiable formulas quickly, but cannot prove that none exists^[10].

(* Graph colouring as SAT: variable x(v,c) says vertex v has colour c. *)
let colouring ~vertices ~edges ~colours =
  let x v c = (v * colours) + c + 1 in
  let some_colour = List.init vertices (fun v -> List.init colours (x v)) in
  let one_colour = List.concat (List.init vertices (fun v ->
      List.concat (List.init colours (fun c ->
          List.init (colours - c - 1) (fun d -> [ - (x v c); - (x v (c + d + 1)) ]))))) in
  let proper = List.concat_map (fun (u, v) -> List.init colours (fun c -> [ - (x u c); - (x v c) ])) edges in
  (Cnf.of_clauses (some_colour @ one_colour @ proper), fun model v ->
      List.find (fun c -> model.(x v c)) (List.init colours Fun.id))
 
(* The Petersen graph: an outer 5-cycle, an inner pentagram, and spokes. *)
let petersen =
  List.init 5 (fun i -> (i, (i + 1) mod 5)) @ List.init 5 (fun i -> (5 + i, 5 + ((i + 2) mod 5)))
  @ List.init 5 (fun i -> (i, i + 5))

Petersen graph, 2 colours: 20 variables, 50 clauses: impossible
Petersen graph, 3 colours: 30 variables, 85 clauses: 2 1 2 1 0 1 2 0 0 1

The same pattern, variables for the choices and clauses for the constraints, encodes scheduling, planning^[15], circuit equivalence and puzzle solving. For bounded model checking, the states of a system over $k$ steps become variables and a satisfying assignment is a trace that violates the property^[12].

Random $k$-SAT formulas, with $m$ clauses chosen uniformly among those of $k$ distinct variables, show a sharp phase transition. For 3-SAT, formulas with fewer than about 4.27 clauses per variable are almost always satisfiable when $n$ is large, and formulas with more are almost always unsatisfiable^[9][17]. The hardest formulas for complete solvers lie at the threshold: below it, satisfying assignments are plentiful and easy to find; above it, contradictions are dense and quickly found.

(* Random 3-SAT with n variables and m = r n clauses: how often is it
   satisfiable, and how hard is it to decide? *)
let median l = let a = Array.of_list (List.sort compare l) in a.(Array.length a / 2)

ratio  n=50 sat  n=150 sat  n=150 median conflicts
 3.00      100%       100%           4
 3.50      100%       100%          31
 3.80       98%       100%         188
 4.00       90%        94%         580
 4.20       65%        62%        1857
 4.30       51%        41%        2059
 4.40       38%        25%        2158
 4.60       27%         2%        1910
 5.00        5%         0%        1122
 5.50        0%         0%         745
 6.00        0%         0%         503

Mitchell, Selman and Levesque observed the easy–hard–easy pattern in 1992^[9]. Statistical physicists predicted the 3-SAT threshold at 4.267 and designed survey propagation, an algorithm that solves random formulas very close to it^[17]. Ding, Sly and Sun proved that the threshold exists and determined its value for all sufficiently large $k$ in 2015^[16]; for $k=3$ it remains a conjecture.

A satisfying assignment is its own certificate. An unsatisfiability claim needs a proof, and the annual SAT competition requires solvers to emit one, usually in the DRAT format, a sequence of clause additions and deletions, each of which a separate checker can verify in polynomial time in the size of the proof^[14]. Proofs can be enormous. The Boolean Pythagorean triples problem, whether the integers from 1 to 7825 can be split into two parts neither of which contains a Pythagorean triple, was settled negatively in 2016 with a DRAT proof of about 200 terabytes^[13].

Davis and Putnam gave a procedure for propositional satisfiability in 1960 as part of a method for first-order logic, based on eliminating variables by resolution^[4]; Davis, Logemann and Loveland replaced the elimination by backtracking search in 1962^[5]. Cook's 1971 paper introduced NP-completeness with SAT as its first example^[1], and Levin found the same result independently in the Soviet Union^[2]. Practical solving advanced slowly until the 1990s: local search methods appeared in 1992 and 1994^[10], GRASP introduced conflict-driven clause learning in 1996^[6], and Chaff's watched literals and VSIDS in 2001 made solvers one to two orders of magnitude faster^[7]. MiniSat, published in 2003, became the standard small solver on which many others were built^[8]. SAT competitions have been held since 2002, and the Handbook of Satisfiability collects the field^[3].

• CNFA propositional formula is in conjunctive normal form (CNF) when it is a conjunction of clauses, each clause a disjunction of literals, and each literal a variable or its negation. Every formula is equivalent to one in CNF, but the equivalent CNF can be exponentially larger; the Tseitin transformation instead produces an equisatisfiable CNF of linear size by adding variables. CNF is the input format of SAT solvers and resolution provers, and restricted forms such as Horn clauses and 2-CNF can be solved in linear time.
• DPLLDPLL, the Davis–Putnam–Logemann–Loveland procedure, is the backtracking search algorithm for Boolean satisfiability on which all complete SAT solvers are built. It repeatedly simplifies a CNF formula by unit propagation and pure literal elimination, then chooses an unassigned variable and tries both of its values in turn, backtracking to the most recent choice when a clause becomes false. It is sound and complete, uses memory linear in the formula, and its runs on unsatisfiable formulas correspond to tree-like resolution proofs, which gives exponential lower bounds such as the n! − 1 decisions it needs for the pigeonhole formulas. Clause learning turned it into CDCL.
• CDCLConflict-driven clause learning (CDCL) is the algorithm of modern SAT solvers. It extends DPLL backtracking search with three ideas: when propagation falsifies a clause, conflict analysis derives a new clause that explains the conflict and adds it to the formula; the solver then backjumps non-chronologically to the decision level at which the new clause forces a literal; and branching follows the variables involved in recent conflicts. With watched literals, restarts and clause deletion, CDCL solvers decide industrial formulas with millions of variables, and with restarts they are as strong as general resolution, exponentially stronger than DPLL.
• DIMACS CNFDIMACS CNF is the standard plain-text format for Boolean formulas in conjunctive normal form, read by essentially every SAT solver. After optional comment lines beginning with c, a header p cnf V C gives the number of variables and clauses; each clause is then a list of non-zero integers, v for a variable and −v for its negation, terminated by 0. It was defined for the Second DIMACS Implementation Challenge in 1993 and has variants for quantified formulas (QDIMACS), weighted MaxSAT (WCNF) and unsatisfiability proofs (DRAT).
• Tseitin transformationThe Tseitin transformation converts an arbitrary propositional formula or Boolean circuit into conjunctive normal form in linear time by introducing a new variable for each subformula and adding a few clauses that define it as the result of its operator: g ↔ a ∧ b becomes (¬g ∨ a), (¬g ∨ b) and (g ∨ ¬a ∨ ¬b). The result is not equivalent to the original formula but equisatisfiable, and every model of one extends or restricts to a model of the other. It is how SAT solvers receive circuits and structured formulas; the Plaisted–Greenbaum variant emits only the implications required by each subformula's polarity, roughly halving the clauses.
• SMTSatisfiability modulo theories (SMT) is the problem of deciding whether a first-order formula is satisfiable when some of its symbols are interpreted by background theories, such as integer or real arithmetic, bit-vectors, arrays and uninterpreted functions. SMT solvers such as Z3 and cvc5 combine a SAT solver, which handles the Boolean structure, with specialized decision procedures for the theories, usually in the DPLL(T) architecture. They read the standard SMT-LIB language and are the reasoning engines of program verifiers, symbolic execution tools, test generators and many other analysis tools.
• Pigeonhole formulaThe pigeonhole formulas PHPⁿ⁺¹ₙ are CNF formulas stating that n + 1 pigeons can be placed in n holes with no two in the same hole. They are unsatisfiable, as the pigeonhole principle says, but Haken proved in 1985 that every resolution refutation of them has exponential size. Since SAT solvers based on DPLL and CDCL produce resolution proofs, they need exponential time on these small formulas, which makes the family the standard example of what resolution cannot do. Proof systems that can count, such as cutting planes and extended resolution, refute them in polynomial size.
• 2-SAT2-SAT is Boolean satisfiability restricted to formulas in conjunctive normal form whose clauses have at most two literals. Unlike 3-SAT it is solvable in linear time: each clause (a or b) is a pair of implications, not a implies b and not b implies a, and the formula is unsatisfiable exactly when some variable and its negation lie in the same strongly connected component of the resulting implication graph. A satisfying assignment can be read off a topological order of the components. Random 2-SAT has a sharp satisfiability threshold at one clause per variable.
• Bit-blastingBit-blasting decides formulas over fixed-width bit-vectors, the machine integers of programs and hardware, by translating every variable into one Boolean variable per bit and every operation into a Boolean circuit, then handing the resulting clauses to a SAT solver. Addition becomes a ripple-carry adder and multiplication a shift-and-add array of adders, encoded with the Tseitin transformation. It is complete and simple, and it is how SMT solvers handle bit-vectors after word-level simplification; its weak point is multiplication, whose circuits are large and hard for SAT solvers.
• Craig interpolationCraig's interpolation theorem states that if a formula A implies a formula B, there is a formula I, the interpolant, built only from the symbols A and B have in common, such that A implies I and I implies B. In verification it is used in the equivalent refutation form: when A ∧ B is unsatisfiable, an interpolant is implied by A, inconsistent with B, and mentions only shared variables. For propositional logic, an interpolant can be computed from a resolution refutation of A ∧ B in linear time, which McMillan used in 2003 to build an unbounded model checker from a SAT solver.

• Implementing SAT in OCaml Part 1CNF, unit propagation, a full recursive DPLL solver, pure literal elimination, a DIMACS parser, and a command-line driver.
• Implementing SAT in OCaml Part 3From SAT to SMT: the DPLL(T) architecture, reusing conflict-driven learning for theory conflicts, and a union-find equality theory.

1. [1]S. A. Cook, “The complexity of theorem-proving procedures”, STOC (1971).
2. [2]L. A. Levin, “Universal sequential search problems”, Problems of Information Transmission 9 (1973).
3. [3]A. Biere, M. Heule, H. van Maaren, T. Walsh (eds.), Handbook of Satisfiability, IOS Press (2nd ed., 2021).
4. [4]M. Davis, H. Putnam, “A computing procedure for quantification theory”, Journal of the ACM 7 (1960).
5. [5]M. Davis, G. Logemann, D. Loveland, “A machine program for theorem-proving”, Communications of the ACM 5 (1962).
6. [6]J. P. Marques-Silva, K. A. Sakallah, “GRASP: a search algorithm for propositional satisfiability”, IEEE Transactions on Computers 48 (1999).
7. [7]M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, “Chaff: engineering an efficient SAT solver”, DAC (2001).
8. [8]N. Eén, N. Sörensson, “An extensible SAT-solver”, SAT, Lecture Notes in Computer Science 2919 (2004).
9. [9]D. Mitchell, B. Selman, H. Levesque, “Hard and easy distributions of SAT problems”, AAAI (1992).
10. [10]B. Selman, H. Kautz, B. Cohen, “Noise strategies for improving local search”, AAAI (1994).
11. [11]T. J. Schaefer, “The complexity of satisfiability problems”, STOC (1978).
12. [12]A. Biere, A. Cimatti, E. Clarke, Y. Zhu, “Symbolic model checking without BDDs”, TACAS (1999).
13. [13]M. J. H. Heule, O. Kullmann, V. W. Marek, “Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer”, SAT (2016).
14. [14]N. Wetzler, M. J. H. Heule, W. A. Hunt, “DRAT-trim: efficient checking and trimming using expressive clausal proofs”, SAT (2014).
15. [15]H. Kautz, B. Selman, “Planning as satisfiability”, ECAI (1992).
16. [16]J. Ding, A. Sly, N. Sun, “Proof of the satisfiability conjecture for large k”, STOC (2015).
17. [17]M. Mézard, G. Parisi, R. Zecchina, “Analytic and algorithmic solution of random satisfiability problems”, Science 297 (2002).
18. [18]B. Aspvall, M. F. Plass, R. E. Tarjan, “A linear-time algorithm for testing the truth of certain quantified Boolean formulas”, Information Processing Letters 8 (1979).
19. [19]R. M. Karp, “Reducibility among combinatorial problems”, in Complexity of Computer Computations, Plenum (1972).

last updated 28 September 2026