Boolean Satisfiability Problem

The Boolean satisfiability problem, usually abbreviated SAT, is the problem of determining whether a formula in propositional logic can be made true by assigning truth values to its variables. A formula with at least one such assignment is satisfiable; one with none is unsatisfiable. SAT is a fundamental problem in computer science: it was the first problem established as NP-complete, and it provides a general framework for expressing and solving many finite constraint problems. (cs.princeton.edu)

Definition and logical meaning

A Boolean formula consists of variables taking the values true and false, combined with connectives such as negation ( $\neg$ ), conjunction ( $\land$ ), and disjunction ( $\lor$ ). A truth assignment specifies a value for each variable. SAT asks whether there exists an assignment under which the entire formula evaluates to true. (arxiv.org)

For a formula $F$ with variables $x_1,\ldots,x_n$ , this can be written as

\exists a\in\{0,1\}^{n}\quad F(a)=1,

where $0$ represents false and $1$ represents true. An assignment satisfying the formula is also called a model. (theory.cs.princeton.edu)

For example,

F=(x\lor y)\land(\neg x\lor z)\land\neg z

is satisfiable: setting $x=0$ , $y=1$ , and $z=0$ makes every conjunct true. By contrast,

G=x\land\neg x

is unsatisfiable because its two conjuncts require incompatible values of $x$ .

Satisfiability differs from validity. A satisfiable formula is true under at least one assignment; a valid formula, or tautology, is true under every assignment. These notions are related by negation: $F$ is valid exactly when $\neg F$ is unsatisfiable. Thus, checking whether premises entail a conclusion can be reduced to checking that the premises together with the negated conclusion are unsatisfiable. (arxiv.org)

Conjunctive normal form and encodings

SAT solvers commonly operate on formulas in conjunctive normal form (CNF). A literal is a variable or its negation; a clause is a disjunction of literals; and a CNF formula is a conjunction of clauses:

F=\bigwedge_{i=1}^{m}C_i, \qquad C_i=\bigvee_{j=1}^{k_i}\ell_{ij}.

A satisfying assignment must make at least one literal true in every clause. This representation supports efficient storage and manipulation as a list of clauses, each containing a list of literals. (theory.cs.princeton.edu)

Converting an arbitrary formula into a logically equivalent CNF by repeatedly distributing disjunction over conjunction can produce an exponentially larger expression. The Tseitin transformation avoids this growth by introducing auxiliary variables representing subformulas and adding clauses that enforce their definitions. The resulting CNF has size linear in the original expression, under the usual bounded-arity representation, and is equisatisfiable with it. (cs.cmu.edu)

Equisatisfiability preserves whether a solution exists, rather than requiring identical assignments over identical variable sets. A definitional encoding permits satisfying assignments to the original variables to be extended to auxiliary variables, and models of the encoding to be projected back to the original variables. (cs.cmu.edu)

Encoding choices matter in practice. Two encodings of the same constraint may differ in size, propagation strength, and solver performance. A smaller encoding is not necessarily easier to solve. (cs.cmu.edu)

Computational complexity and historical significance

SAT occupies a central position in computational complexity. Stephen Cook established its foundational completeness result in 1971; Leonid Levin independently obtained related results published in 1973. The result is known as the Cook–Levin theorem. (theory.stanford.edu)

Its modern formulation has two parts:

SAT belongs to NP: a proposed satisfying assignment can be checked in time polynomial in the formula’s size.
SAT is NP-hard: every decision problem in NP can be transformed into SAT by a polynomial-time reduction preserving the answer. (theory.cs.princeton.edu)

The theorem connects computation with logic. A polynomially bounded computation can be represented by Boolean constraints describing its initial configuration, legal transitions, and accepting outcome. Those constraints are satisfiable exactly when an accepting computation exists. (cs.princeton.edu)

Consequently, a polynomial-time algorithm for general SAT would imply $P=NP$ ; conversely, $P=NP$ would imply such an algorithm exists. NP-completeness is a worst-case classification, not a claim that every SAT instance is difficult. (cs.princeton.edu)

SAT is formally a decision problem, whose answer is yes or no. Solvers generally also return a satisfying assignment when one exists. Decision and search are closely related: given a SAT decision procedure, a model can be constructed by fixing variables one at a time and testing whether satisfiability is retained. (theory.cs.princeton.edu)

Important restricted forms

Restrictions on formula structure can change the problem’s complexity substantially.

3-SAT restricts CNF clauses to at most three literals. It remains NP-complete, and is widely used in complexity reductions. Long clauses can be replaced by chains of short clauses using auxiliary variables without losing satisfiability. (theory.cs.princeton.edu)

2-SAT permits at most two literals per clause and is solvable in polynomial time. A clause $a\lor b$ can be interpreted as the implications $\neg a\Rightarrow b$ and $\neg b\Rightarrow a$ . This leads to an implication-graph method: the formula is unsatisfiable precisely when a variable and its negation belong to the same strongly connected component. (cs.princeton.edu)

Horn-SAT restricts each clause to at most one positive literal. Such clauses can express implication rules, allowing forced truth values to be propagated systematically. Horn satisfiability is decidable in linear time in the total number of literal occurrences. (seas.upenn.edu)

Disjunctive-normal-form satisfiability is also tractable: a disjunction of conjunctions is satisfiable if at least one conjunction contains no contradictory pair of literals. However, converting an arbitrary formula to this representation may require exponential space, so this does not yield an efficient general SAT procedure. (cs.cmu.edu)

Solving methods

Exhaustive search and DPLL

A direct method constructs a truth table or otherwise tests all $2^n$ assignments to $n$ variables. It is complete but scales exponentially with the number of variables. More effective methods avoid exploring assignments already ruled out by constraints. (cs.cmu.edu)

The Davis–Putnam–Logemann–Loveland algorithm (DPLL), introduced in 1962, combines branching with simplification. It repeatedly applies unit propagation: if a clause has only one literal not already false, that literal must be true. When propagation does not settle the formula, the algorithm selects an unassigned variable, tries a value, and backtracks if a clause becomes false. (cs.cmu.edu)

Conflict-driven clause learning

Conflict-driven clause learning (CDCL) extends this search process by analyzing conflicts and deriving new clauses that prevent their causes from recurring. Rather than merely undoing the last decision, a solver can backjump to an earlier relevant decision level. (cs.cmu.edu)

CDCL implementations combine clause learning with efficient propagation, branching heuristics, restarts, and deletion of selected learned clauses. Restarts abandon the current partial assignment while retaining useful learned information. These techniques guide search without changing the underlying logical question. (cs.cmu.edu)

Local search

Local-search methods begin with a complete assignment and repeatedly change variable values to reduce the number of unsatisfied clauses. They may find satisfying assignments effectively, but failure to find one within a time limit does not establish unsatisfiability. This distinguishes them from complete procedures capable, given sufficient resources, of settling either outcome. (cs.cmu.edu)

Applications and result verification

SAT is used as a general-purpose engine by translating a problem into Boolean constraints. Applications include hardware and software formal verification, automated planning, and scheduling. In verification, constraints may describe a system execution that violates a required property; a satisfying assignment then represents a counterexample. (cs.cmu.edu)

A satisfiable result can be checked by evaluating the returned assignment against the input formula. An unsatisfiable result requires a different kind of evidence: a proof that no satisfying assignment exists. SAT solvers can produce proof logs in formats such as DRAT and LRAT, which separate complex proof generation from independent checking. LRAT adds hints that facilitate relatively simple, efficient checkers, including implementations verified using theorem-proving systems. (cs.cmu.edu)

Proof checking validates the encoded formula’s unsatisfiability. The correctness of the translation from the original application remains a separate obligation; an incorrectly encoded system can yield a correct SAT result about the wrong problem. (cs.cmu.edu)

Extensions and related problems

Several related problems preserve Boolean reasoning while changing the question or adding expressive power.

Maximum satisfiability (MaxSAT) asks for an assignment satisfying as many clauses as possible. Weighted variants maximize the total weight of satisfied clauses; partial variants distinguish mandatory hard clauses from optional soft clauses. These are optimization problems rather than simply feasibility tests. (cs.cmu.edu)
Model counting ( $\#\mathrm{SAT}$ ) asks how many assignments satisfy a formula. It is a counting problem and is $\#P$ -complete. Finding one model is generally insufficient for determining the total number of models. (cs.cornell.edu)
Quantified Boolean formulas (QBF) allow both existential and universal quantifiers. Ordinary SAT corresponds to existentially quantifying every variable; deciding the truth of unrestricted closed QBFs is PSPACE-complete. Quantifier order determines which existential choices may depend on preceding universal choices. (cs.cmu.edu)
Satisfiability modulo theories (SMT) combines Boolean structure with interpreted constraints, such as arithmetic, arrays, or bit vectors. Many SMT solvers coordinate a Boolean solver with specialized theory procedures; complexity and decidability depend on the theories and formula fragments involved. (arxiv.org)

Practical limitations

Effective SAT solving does not remove worst-case computational difficulty. Performance depends on the instance’s structure, the encoding, and the solver’s search strategy. Even constraints with efficient specialized algorithms may be awkward for a general Boolean solver when their structure is poorly exposed by the encoding. (cs.cmu.edu)

Resource limits also affect the meaning of reported outcomes. A timeout or an “unknown” result means that the computation has not settled the question; it is not evidence of unsatisfiability. Likewise, the scope of a verification result is determined by the encoded model and its bounds, not merely by the solver’s ability to answer SAT or UNSAT. (cs.cmu.edu)

References

Cook-Levin Theorem: SAT is NP-completecs.princeton.edu
Intractability IIcs.princeton.edu
Lecture: SAT & SMT, Part 2cs.cmu.edu
The Complexity of Theorem-Proving Procedurestheory.stanford.edu
Computational Complexity: A Modern Approachtheory.cs.princeton.edu
A Survey of Satisfiability Modulo Theoryarxiv.org
Verified CNF Encodingscs.cmu.edu
Logic and Mechanized Reasoning: SAT Basicscs.cmu.edu
Lecture 23: Intractabilitycs.princeton.edu
Chapter 18 — Horn and 2-SAT Satisfiability (Classical)users.ece.utexas.edu
Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulaeseas.upenn.edu
Generalizing Boolean Satisfiability I: Introductioncs.cmu.edu