Boolean satisfiability problem

The Boolean satisfiability problem (often abbreviated SAT) is the problem of determining whether a given propositional formula has an assignment of truth values to its variables that makes the entire formula true. Despite its simplicity, SAT is the canonical NP-complete problem: every problem whose solutions can be verified in polynomial time reduces to SAT in polynomial time, as proved by the Cook-Levin theorem.

SAT is typically studied in conjunctive normal form (CNF), where the formula is a conjunction of clauses, each clause being a disjunction of literals. The special case where each clause contains exactly three literals — 3-SAT — remains NP-complete and is the standard form for theoretical analysis. In practice, modern SAT solvers routinely handle formulas with millions of variables and clauses, exploiting structure that worst-case analysis cannot capture.

The problem sits at the center of computer science because it is simultaneously the hardest problem in NP and the most practically tractable. Hardware verification, automated planning, cryptanalysis, and constraint satisfaction all reduce to SAT. The gap between SAT's theoretical intractability and its empirical solvability is one of the most instructive cases in the study of P versus NP: worst-case hardness is a statement about all possible inputs, while practical success is a statement about the inputs that actually arise in engineering.

SAT in Hardware Verification

The industrial application of SAT that transformed the field is hardware verification. Modern microprocessors contain billions of transistors and operate at frequencies where a single design bug can cost hundreds of millions of dollars. Simulation-based testing cannot cover the exponential space of possible inputs and states. Formal verification using SAT solvers provides a mathematical guarantee: the design satisfies its specification for all possible inputs, or the solver produces a counterexample.

The methodology, pioneered in the 1990s and now standard practice at companies like Intel, AMD, and ARM, encodes the processor design and its specification as a Boolean formula. The formula is satisfiable if and only if there exists an input that causes the design to violate the specification. SAT solvers have caught bugs in floating-point units, memory controllers, and cache coherence protocols — bugs that simulation missed because they required precise sequences of operations spanning thousands of cycles.

SAT in Automated Reasoning

Beyond hardware, SAT solvers are the engine of modern automated reasoning. SMT solvers extend SAT to arithmetic, arrays, and uninterpreted functions, enabling verification of software programs, cryptographic protocols, and distributed systems. The DPLL algorithm, the ancestor of modern CDCL solvers, was originally designed for automated theorem proving in the 1960s. Its evolution from a theoretical curiosity to an industrial tool is one of the great success stories of applied logic.

SAT is also the foundation of MaxSAT and Pseudo-Boolean Optimization, variants that ask not just whether a formula is satisfiable but how many clauses can be satisfied simultaneously, or what assignment optimizes a linear objective. These extensions have transformed SAT from a decision problem into an optimization framework, with applications in scheduling, routing, and resource allocation.

SAT is not merely a problem. It is a mirror. Every domain that deals with constraints — scheduling, verification, design — sees its own face reflected in the Boolean variables and clauses of satisfiability. The universality of SAT is not a mathematical curiosity; it is evidence that constraint satisfaction is the fundamental pattern underlying computation itself. The fact that SAT is both theoretically intractable and practically indispensable is not a paradox. It is a lesson: that the boundary between impossible and possible is not where the theorems place it, but where the structure of real problems redraws it.