Boolean satisfiability problem
The Boolean satisfiability problem (SAT) is the fundamental decision problem in computational logic and complexity theory that asks whether there exists an assignment of truth values (true or false) to the variables in a given Boolean formula such that the formula evaluates to true.[1] Typically formulated in conjunctive normal form (CNF), where the formula is a conjunction of clauses each being a disjunction of literals (variables or their negations), SAT determines the satisfiability of such expressions, with unsatisfiability implying a contradiction in the propositional logic represented by the formula.[1] Proven to be NP-complete by Stephen A. Cook in his 1971 paper "The Complexity of Theorem-Proving Procedures," SAT serves as the canonical example for the NP complexity class, meaning any problem in NP can be reduced to SAT in polynomial time, and it underpins the unsolved P vs. NP question central to theoretical computer science.[2] This NP-completeness result, the first of its kind, sparked the development of the entire field of NP-completeness, influencing reductions for thousands of other problems across mathematics, optimization, and engineering.[2] Despite its theoretical intractability—requiring exponential time in the worst case for exact solutions—modern SAT solvers employ advanced heuristics, conflict-driven clause learning, and branch-and-bound techniques derived from the Davis–Putnam–Logemann–Loveland (DPLL) algorithm (introduced in 1962), enabling them to resolve industrial-scale instances with millions of variables and clauses in seconds.[1] These solvers power diverse applications, including hardware and software verification (e.g., checking circuit equivalence or bug detection), artificial intelligence planning (e.g., automated scheduling), operations research (e.g., constraint satisfaction in logistics), and bioinformatics (e.g., protein folding models), demonstrating a remarkable gap between worst-case theory and practical performance.[1] Annual international SAT competitions since 2002 have accelerated progress, akin to "Moore's Law" for SAT solving, with empirical studies revealing that real-world instances often exhibit structure exploitable by machine learning and preprocessing techniques.[1] Variants like 2-SAT (linear-time solvable) and 3-SAT (NP-complete even for clauses of three literals) highlight the problem's parameterized complexity, while extensions to quantified Boolean formulas (QBF) address higher levels of the polynomial hierarchy.[1]Definitions and Formalism
Boolean Formulas
In propositional logic, the fundamental building blocks are propositional variables, also known as Boolean variables, which represent atomic propositions that can take one of two truth values: true (often denoted as T or 1) or false (F or 0).[3] These variables, typically denoted by lowercase letters such as p, q, r, do not possess internal structure and serve as placeholders for declarative statements whose truth values are to be evaluated.[3] Propositional formulas are constructed using a set of logical connectives that combine these variables to form more complex expressions. The primary connectives include negation (\neg), conjunction (\land), disjunction (\lor), implication (\rightarrow), and biconditional (\leftrightarrow). Each connective defines a truth-functional operation, meaning the truth value of the resulting formula depends solely on the truth values of its components, as specified by their truth tables.[4] The truth table for negation (\neg A) is:| A | \neg A |
|---|---|
| T | F |
| F | T |
| A | B | A \land B |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | F |
| F | F | F |
| A | B | A \lor B |
|---|---|---|
| T | T | T |
| T | F | T |
| F | T | T |
| F | F | F |
| A | B | A \rightarrow B |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | T |
| F | F | T |
| A | B | A \leftrightarrow B |
|---|---|---|
| T | T | T |
| T | F | F |
| F | T | F |
| F | F | T |
Satisfiability and Models
In propositional logic, a satisfying assignment for a Boolean formula \phi is a function that assigns truth values (true or false) to each propositional variable in \phi such that the entire formula evaluates to true.[2] Any such satisfying assignment is also called a model of \phi.[2] If no satisfying assignment exists for \phi, the formula is unsatisfiable, meaning it evaluates to false under every possible assignment of truth values to its variables.[2] The Boolean satisfiability problem (SAT) is the fundamental decision problem in this context: given a Boolean formula \phi over a finite set of propositional variables, determine whether there exists at least one satisfying assignment (model) for \phi.[2] Formally, SAT asks if \phi is satisfiable, with a "yes" instance admitting at least one model and a "no" instance being unsatisfiable.[2] For a formula with n distinct variables, the total number of possible assignments is $2^n, representing the exhaustive search space to check for satisfiability.[7] To illustrate, consider the Boolean formula \phi = (p \lor \neg q) \land (\neg p \lor r). One satisfying assignment is p = \false, q = \false, r = \true: here, p \lor \neg q evaluates to \false \lor \true = \true, and \neg p \lor r evaluates to \true \lor \true = \true, so \phi is \true \land \true = \true.[2] Special cases arise with tautologies and contradictions. A tautology is a formula that evaluates to true under every possible assignment, meaning every assignment is a model (e.g., p \lor \neg p).[8] Conversely, a contradiction is a formula that evaluates to false under every assignment, having no models (e.g., p \land \neg p).[8] These represent the extreme ends of satisfiability: universal satisfaction for tautologies and complete unsatisfiability for contradictions.[8]Conjunctive Normal Form
In Boolean logic, a literal is either a Boolean variable x_i or its negation \neg x_i.[9] A clause is a disjunction (logical OR) of one or more literals, such as x_1 \lor \neg x_2 \lor x_3.[9] A Boolean formula is in conjunctive normal form (CNF) if it is a conjunction (logical AND) of one or more clauses, for example, (x_1 \lor \neg x_2) \land (\neg x_1 \lor x_3 \lor \neg x_4).[9] This representation is the standard input format for the Boolean satisfiability problem (SAT), as it structures the formula into a product of sums that facilitates analysis of satisfying assignments.[10] The clause width of a CNF formula refers to the maximum number of literals in any clause; for instance, a formula in 3-CNF has clauses with at most three literals each.[11] More generally, a k-CNF formula restricts all clauses to have at most (or, in some contexts, exactly) k literals, which controls the structural complexity and is central to variants like 2-SAT or 3-SAT.[11] Any general Boolean formula can be converted to an equivalent CNF formula using a systematic process: first, eliminate non-standard connectives like implication (p \to q \equiv \neg p \lor q) and biconditional by replacing them with disjunctions; second, apply double negation elimination and De Morgan's laws to push negations inward to literals; finally, use the distributive law to expand any remaining conjunctions over disjunctions, yielding a conjunction of clauses.[12] For example, the implication p \to q directly converts to the single clause \neg p \lor q, which is already in CNF.[12] However, this conversion can result in an exponential increase in formula size, as distributing over multiple terms may produce up to $2^n clauses for certain inputs with n variables.[12]Computational Complexity
NP-Completeness
The Boolean satisfiability problem (SAT) belongs to the complexity class NP because, given a Boolean formula in conjunctive normal form and a candidate assignment of truth values to its variables, one can verify whether the assignment satisfies the formula in polynomial time by evaluating each clause individually.[13] The NP-hardness of SAT is established by the Cook-Levin theorem, which provides a polynomial-time reduction from any problem in NP to SAT.[13] To show this, consider an arbitrary language L \in \mathrm{NP}; by definition, there exists a nondeterministic Turing machine M that decides L in polynomial time, say p(n) steps on inputs of length n. For an input string w of length n, the reduction constructs a Boolean formula \phi_{M,w} in CNF such that \phi_{M,w} is satisfiable if and only if M accepts w. The construction encodes the possible computation paths of M on w using Boolean variables that represent the state of the tape, head position, and machine state at each of the p(n) time steps. Specifically, variables are defined for each possible symbol in each tape cell at each time step, ensuring the formula size remains polynomial in n. Clauses in \phi_{M,w} enforce three key properties: (1) the initial configuration matches w on the input tape with the head at the starting position and initial state; (2) consecutive configurations adhere to M's transition rules, allowing changes in at most a constant number of adjacent tape cells per step; and (3) at least one computation path ends in an accepting configuration after at most p(n) steps. This encoding simulates the nondeterministic choices and verifications of M, reducing the acceptance problem to satisfiability.[13] The Cook-Levin theorem implies that every problem in NP can be reduced to SAT in polynomial time, making SAT the first problem proven to be NP-complete and providing a canonical hard problem for the class.[13] This result, originally proven by Stephen Cook in his 1971 paper "The Complexity of Theorem-Proving Procedures," formalized the notion of NP-completeness and profoundly influenced computational complexity theory by enabling reductions from SAT to establish hardness for numerous other problems.[13] Independently, Leonid Levin developed a similar proof around the same time, though it was published later in the West.k-SAT and Clause Width
The k-SAT problem is a restriction of the Boolean satisfiability problem to conjunctive normal form formulas in which every clause consists of exactly k literals, where each literal is a variable or its negation.[10] The cases k=1 and k=2 are solvable in polynomial time. For k=1, each clause is a unit clause of the form (x) or (¬x), and the formula is satisfiable unless a variable and its negation both appear as clauses; this can be checked and resolved in linear time by propagating forced assignments.[10] For k=2, 2-SAT instances can be solved in linear time via construction of an implication graph, where vertices represent literals and edges encode implications between clauses, followed by detection of strongly connected components to identify contradictions.[14] In contrast, k-SAT is NP-complete for every fixed k ≥ 3.[15] Since 3-SAT is NP-complete, the result for larger k follows from a polynomial-time reduction from (k-1)-SAT to k-SAT, applied recursively from 3-SAT. Specifically, given a (k-1)-clause C = (ℓ1 ∨ ⋯ ∨ ℓk-1), introduce a fresh variable y and replace C with the two k-clauses (\ell_1 \vee \cdots \vee \ell_{k-1} \vee y) \wedge (\ell_1 \vee \cdots \vee \ell_{k-1} \vee \neg y). This preserves satisfiability: if C is falsified, both new clauses require contradictory values for y; if C is satisfied, both hold regardless of y. Each original clause thus generates a constant number of new clauses and variables, yielding a polynomial-size k-CNF formula equivalent to the input.[15] The case k=3, known as 3-SAT, is the paradigmatic hard instance of k-SAT and underpins much of the theory of NP-hardness. Beyond NP-completeness, finer-grained hardness results stem from the Exponential Time Hypothesis (ETH), which asserts that no algorithm solves n-variable 3-SAT in time 2o(n).[16] Using sparsification techniques, ETH implies concrete lower bounds on the exponential base. Under ETH, 3-SAT cannot be solved in subexponential time 2^{o(n)}. Current best algorithms achieve O(1.307^n) time (randomized) or O(1.328^n) time (deterministic) as of 2021, highlighting the gap between theoretical lower bounds and practical algorithms.[17] These bounds highlight that exact solving remains computationally intensive even for moderate instance sizes, influencing algorithm design and parameterized complexity. Random instances of 3-SAT exhibit a phase transition in satisfiability as a function of the clause-to-variable ratio α = m/n. Empirical investigations show that for α ≲ 4.26, uniformly random 3-CNF formulas with n variables and m = αn clauses are satisfiable with probability approaching 1 as n → ∞; for α ≳ 4.26, they are unsatisfiable with high probability. This threshold, refined through large-scale experiments, demarcates easy-to-satisfy underconstrained regimes from overconstrained unsatisfiable ones, with peak hardness near the transition due to exponentially many near-solutions.[18]Schaefer's Dichotomy Theorem
Schaefer's Dichotomy Theorem, established in 1978, classifies the computational complexity of generalized Boolean satisfiability problems parameterized by a finite set S of Boolean relations, where each relation in S is a subset of \{0,1\}^n for some arity n. The problem SAT(S) asks whether a given conjunction of relational constraints from S (with variables ranging over Boolean values) admits a satisfying assignment. The theorem asserts that SAT(S) is either solvable in polynomial time or is NP-complete, providing a sharp dichotomy based on structural properties of S. This result extends the classical CNF-SAT framework by allowing arbitrary relational constraints rather than solely disjunctive clauses, yet maintains the same complexity boundary.[19] The polynomial-time cases correspond to six specific classes of S, each admitting an efficient recognition and solving algorithm:- 0-valid: Every relation in S is satisfied by the all-false assignment (all variables set to 0).
- 1-valid: Every relation in S is satisfied by the all-true assignment (all variables set to 1).
- Horn: Every relation in S is definable by a Horn formula, meaning it corresponds to the models of a conjunction of clauses with at most one positive literal each.
- Anti-Horn: The dual of Horn, where every relation corresponds to clauses with at most one negative literal.
- 2-CNF: Every relation in S has width at most 2, equivalent to implications between at most two literals, reducible to 2-SAT.
- Affine: Every relation in S consists of solutions to a system of linear equations over the finite field GF(2), solvable via Gaussian elimination.
Polynomial-Time Solvable Cases
2-SAT
The 2-satisfiability problem, or 2-SAT, restricts the Boolean satisfiability problem to conjunctive normal form formulas where each clause contains exactly two literals. This case is solvable in polynomial time, distinguishing it from the NP-complete general SAT problem.[21] A central technique for solving 2-SAT involves constructing an implication graph. Given a 2-CNF formula \phi with n variables, the graph G has $2n vertices, one for each literal x_i and \neg x_i for i = 1, \dots, n. For every clause (a \lor b) in \phi, where a and b are literals, add directed edges \neg a \to b and \neg b \to a to G. These edges encode the logical implications required for the clause to hold: if \neg a is true, then b must be true, and similarly for the other direction. The resulting graph has at most $2m edges, where m is the number of clauses.[21] The formula \phi is unsatisfiable if and only if there exists a variable x such that x and \neg x lie in the same strongly connected component (SCC) of [G](/page/G). In this case, there are directed paths from x to \neg x and from \neg x to x, implying a contradiction where both x and \neg x must be true. Conversely, if no such pair exists, \phi is satisfiable.[21] The full algorithm proceeds as follows: first, build the implication graph [G](/page/G); second, compute the SCCs of [G](/page/G) using a linear-time method such as Tarjan's algorithm or Kosaraju's algorithm; third, check each variable to see if x and \neg x share an SCC—if any do, declare \phi unsatisfiable. If satisfiable, construct an assignment by obtaining a topological ordering of the SCCs (treating the condensation graph as a DAG). For each variable x, set x to true if the SCC of \neg x precedes the SCC of x in this ordering; otherwise, set x to false. This assignment satisfies all implications, as paths in [G](/page/G) respect the topological order, ensuring no clause is violated.[21] The algorithm runs in O(n + m) time, matching the size of the input formula, since constructing G is linear and SCC computation is linear in the number of vertices and edges.[21] As established by Schaefer's dichotomy theorem, 2-CNF formulas belong to a tractable class within the classification of generalized satisfiability problems, confirming their polynomial-time solvability.[19] For example, consider the 2-CNF formula with clauses (p \lor q), (\neg q \lor r), and (\neg p \lor \neg r). The implication graph includes edges \neg p \to q, \neg q \to p, q \to r, \neg r \to \neg q, p \to \neg r, and r \to \neg p. These form cycles such as p \to \neg r \to \neg q \to p and \neg p \to q \to r \to \neg p, but p and \neg p lie in different SCCs, so the formula is satisfiable. For instance, the assignment p = true, q = false, r = false satisfies all clauses.[21]Horn-SAT
A Horn formula consists of a conjunction of Horn clauses, where each Horn clause is a disjunction of literals containing at most one positive literal.[22] For instance, the clause \neg a \vee \neg b \vee c is a Horn clause, equivalent to the implication (a \wedge b) \to c.[22] Horn-SAT, the problem of determining satisfiability for such formulas, is one of the six tractable classes identified in Schaefer's dichotomy theorem.[19] The satisfiability of a Horn formula can be tested efficiently using a forward chaining algorithm based on unit propagation.[22] This process begins by constructing an implication graph where, for each Horn clause with negative literals \neg x_1, \dots, \neg x_k and positive literal y (or no positive literal for a negative unit clause), directed edges are added from each x_i to y. Unit clauses, which force a variable to true, are identified and propagated: setting a variable v to true removes all clauses containing \neg v (simplifying others by removing \neg v) and adds implications from v to its consequences, using a queue to process assignments in breadth-first order.[22] Propagation continues until no new unit clauses arise; if an empty clause or a cycle forcing a variable both true and false appears, the formula is unsatisfiable.[22] Otherwise, the formula is satisfiable, with all unforced variables set to false yielding a model.[23] If satisfiable, this algorithm uniquely identifies the minimal model, defined as the satisfying assignment with the fewest true variables (or, equivalently, the least model under the componentwise partial order on assignments).[23] The minimal model consists precisely of the variables forced true by propagation, as any satisfying assignment must include these to avoid contradiction, and setting others false preserves satisfiability due to the Horn structure.[23] The algorithm runs in linear time, O(n + m), where n is the number of variables and m the number of clauses, achieved by processing each edge and node in the implication graph at most once via the queue.[22] Example. Consider the Horn formula with clauses (\neg p \vee q), (\neg q \vee r), encoding the implications p \to q and q \to r. Unit propagation yields no initial units, so it is satisfiable with minimal model all false. Adding the unit clause (\neg r) forces r false, but propagation through the reverse implications (from the graph) leads to q false, then p false—no contradiction. However, if instead the positive unit (r) is added along with (\neg r), it would force r true and false, yielding unsatisfiability.[22]Renamable Horn-SAT and Other Tractable Classes
The Boolean satisfiability problem restricted to renamable Horn formulas is solvable in polynomial time. A CNF formula is renamable Horn if there exists a subset of variables whose polarities can be flipped such that the resulting formula is Horn, meaning every clause has at most one positive literal. This class generalizes Horn-SAT, extending tractability to formulas that become Horn after such a renaming. The recognition and satisfiability of renamable Horn formulas can be decided in linear time.[24] The algorithm models the renaming choice as a 2-SAT instance. For each variable x_i, introduce a new variable f_i indicating whether x_i is flipped (f_i = \top means flip). For every original clause, construct binary clauses ensuring that, after the implied renaming, the clause has at most one positive literal. Specifically, for each pair of literals in a clause that could both become positive under some renaming (i.e., both original positives not flipped or both original negatives flipped), add a 2-clause forbidding that pair from both being positive, such as (f_i \lor f_j) or (\neg f_i \lor \neg f_j) depending on the literals. Solving this 2-SAT instance determines if a valid renaming exists; if so, apply the renaming to obtain a Horn formula, then solve it using linear-time unit propagation as in standard Horn-SAT. This reduction leverages the polynomial-time solvability of 2-SAT via implication graphs and strongly connected components.[24] Affine SAT, another tractable class, consists of formulas where all clauses are linear equations over the finite field GF(2, equivalent to XOR clauses (e.g., exclusive-or of literals equal to true or false). Such a formula can be represented as a system of linear equations A \mathbf{x} = \mathbf{b}, where A is an m \times n matrix over GF(2 with rows corresponding to clauses and columns to variables, \mathbf{x} is the variable assignment vector, and \mathbf{b} encodes the required parity (1 for odd number of true literals, 0 for even). Satisfiability is determined by Gaussian elimination on the augmented matrix [A | \mathbf{b}], which runs in O(n^3) time in the worst case for dense systems, or more efficiently for sparse ones. For example, the clause p \oplus q \oplus r (implying an odd number of true variables) corresponds to the equation x_p + x_q + x_r = 1 over GF(2, and solving the full system yields a solution if consistent, or detects inconsistency via rank comparison. This approach directly computes a satisfying assignment when one exists. Schaefer's dichotomy theorem identifies additional tractable classes within its framework: 0-valid formulas, where every clause contains at least one negative literal (satisfied by the all-false assignment); 1-valid formulas, where every clause contains at least one positive literal (satisfied by the all-true assignment); and anti-Horn formulas, the dual of Horn-SAT, consisting of clauses with at most one negative literal (solvable in linear time by duality, mapping to Horn-SAT via negation of all variables).[19] These classes, alongside Horn, affine, and 2-CNF, exhaust the polynomial-time solvable cases under Schaefer's closure properties for generalized SAT. Recognition for these is straightforward: verify clause types directly, with satisfiability following from the respective algorithms (trivial constant assignments for 0-valid and 1-valid, provided no empty clauses).NP-Hard Variants
Exactly-1 3-SAT
The Exactly-1 3-SAT problem, also known as 1-in-3-SAT, is a restricted variant of the Boolean satisfiability problem where the input is a 3-CNF formula, but a satisfying assignment must evaluate exactly one literal to true in every clause, imposing a cardinality constraint of precisely one true literal per clause. This differs from standard 3-SAT, which requires at least one true literal per clause without upper bounds. The problem is in NP, as a candidate assignment can be verified in polynomial time by checking each clause for exactly one true literal. For example, consider the clause (p \lor q \lor r). A satisfying assignment for this clause in Exactly-1 3-SAT must set exactly one of p, q, or r to true and the other two to false; assignments where zero, two, or all three are true would violate the constraint. Exactly-1 3-SAT is NP-hard, established via a polynomial-time reduction from 3-SAT that introduces auxiliary variables to transform the "at least one" condition into "exactly one" by encoding mutual exclusions among literals in each original clause. Specifically, for a 3-SAT clause (x \lor y \lor z), the reduction adds fresh variables to create a set of Exactly-1 3-SAT clauses that are satisfiable if and only if exactly one of x, y, z (or their negations, depending on polarity) is true, ensuring no more than one can hold simultaneously. This construction preserves satisfiability while enforcing the exact cardinality, and the overall transformation is linear in the input size. The positive variant of Exactly-1 3-SAT, where all literals are unnegated, models the exact cover by 3-sets (X3C) problem, an NP-complete set partitioning task where a universe of 3q elements must be exactly covered by disjoint 3-element subsets from a given collection. In this correspondence, variables represent subset selections, and clauses ensure each element appears in exactly one selected subset, directly capturing partitioning constraints. Counting the number of satisfying assignments to an Exactly-1 3-SAT formula is #P-complete, even for the positive case, highlighting the added computational difficulty of enumeration beyond mere existence.Not-All-Equal 3-SAT
The Not-All-Equal 3-SAT (NAE-3-SAT) is a constraint satisfaction problem where the input consists of a conjunction of clauses, each containing exactly three literals over a set of Boolean variables, and a clause is satisfied by a truth assignment if and only if the three literals do not all evaluate to the same truth value—that is, at least one literal is true and at least one is false.[25] This formulation forbids both the all-true (TTT) and all-false (FFF) cases for each clause, distinguishing it from standard 3-SAT, which only requires at least one true literal per clause.[26] A simple example illustrates the satisfaction condition: consider the clause NAE(x_1, \neg x_2, x_3). This clause is satisfied by any assignment where the literals do not all evaluate to true or all to false—for instance, if x_1 = \top, x_2 = \top (making \neg x_2 = \bot), and x_3 = \bot, the values are \top, \bot, \bot (mixed); it is unsatisfied only if all are \top or all \bot.[27] NAE-3-SAT is NP-complete, as established in Schaefer's seminal classification of Boolean constraint satisfaction problems. Even the restricted monotone variant, where all literals are unnegated (positive), remains NP-complete; this version corresponds to ensuring diversity in assignments and can be shown NP-hard by reduction from the graph 3-coloring problem, via equivalence to 2-coloring 3-uniform hypergraphs where no hyperedge is monochromatic (variables as vertices, clauses as hyperedges, true/false as colors).[25][28] In applications, NAE-3-SAT models constraint satisfaction scenarios requiring diversity or non-uniformity among variables, such as in relational databases or logic programming where clauses enforce that not all elements in a tuple share the same value.[29] Regarding parameterized complexity, NAE-3-SAT is fixed-parameter tractable when parameterized by the treewidth of the primal or incidence graph of the formula, admitting algorithms running in time O(2^{O(k)} n) where k is the treewidth and n the input size, similar to general SAT; however, it is W[30]-hard for parameters like the solution size or number of variables in unrestricted cases.[31]Algorithms for Solving SAT
DPLL and Backtracking
The Davis–Putnam–Logemann–Loveland (DPLL) algorithm, introduced in 1962, forms the basis for exact solvers of the Boolean satisfiability problem by combining recursive backtracking search with propositional inference rules to prune the search space efficiently.[32] Developed as a machine-implemented procedure for theorem proving, it takes a propositional formula in conjunctive normal form (CNF) as input and systematically explores partial truth assignments until satisfiability is determined or all possibilities are exhausted.[32] At each step, DPLL first applies simplification techniques to the current formula under a partial assignment: unit propagation and pure literal elimination. Unit propagation identifies clauses reduced to a single unassigned literal (a unit clause) and assigns that literal the value needed to satisfy the clause, then propagates this assignment by substituting into all clauses and repeating until no unit clauses remain or an empty clause (contradiction) arises.[33] Pure literal elimination detects variables that appear only positively (or only negatively) across all remaining clauses and assigns them true (or false, respectively) to satisfy those clauses, removing the affected clauses from consideration.[33] These rules provide sound inference without branching, reducing the formula's size before further decisions. If simplification yields no clauses, the formula is satisfiable under the current partial assignment, and DPLL returns a satisfying assignment by backtracking to complete it. If an empty clause appears, the current branch is unsatisfiable, prompting backtracking to the last decision point. Otherwise, DPLL selects an unassigned variable (typically using a heuristic like most frequent occurrence) and branches by recursing on two subproblems: one assigning the variable true and the other false. This depth-first search continues until a satisfying assignment is found or all branches fail, proving unsatisfiability.[33] Pruning occurs via early termination on contradictions during propagation, avoiding full exploration of doomed subtrees. In the worst case, DPLL exhibits exponential time complexity of O(2^n), where n is the number of variables, as it may need to evaluate all possible truth assignments in a binary decision tree.[34] Despite this, the combination of inference rules and branching heuristics makes it surprisingly effective on structured instances, laying the groundwork for subsequent SAT solver advancements. To illustrate, consider a small 3-SAT instance with variables p, q, r and clauses: (¬p ∨ q), (¬p ∨ r), (q ∨ r), (¬q ∨ ¬r).[33] No initial unit clauses or pure literals exist, so select p for branching.- Branch p = true: Substitute to get (q), (r), (q ∨ r), (¬q ∨ ¬r). Unit propagation sets q = true (from first clause), then r = true (from second). The third clause is satisfied, but the fourth becomes (false ∨ false), yielding an empty clause—unsatisfiable. Backtrack.
- Branch p = false: Substitute to get empty (from first two clauses, satisfied), leaving (q ∨ r), (¬q ∨ ¬r). No units or pures; select q = true: (q ∨ r) is satisfied, (¬q ∨ ¬r) becomes ¬r. Unit propagation sets r = false—no conflict, clauses empty—satisfiable with p=false, q=true, r=false.