Boolean satisfiability problem

The Boolean satisfiability problem (SAT) is the problem of determining whether there exists an assignment of truth values (true or false) to the variables of a given Boolean formula such that the formula evaluates to true. If such an assignment exists, the formula is said to be satisfiable; otherwise, it is unsatisfiable. SAT is a fundamental problem in computer science, logic, and artificial intelligence, and was the first problem proven to be NP-complete.

Definition and formal statement

A Boolean formula is typically expressed in conjunctive normal form (CNF), which is a conjunction (AND) of clauses, where each clause is a disjunction (OR) of literals. A literal is a variable or its negation. For example, (x₁ ∨ ¬x₂) ∧ (x₂ ∨ x₃) ∧ (¬x₁ ∨ ¬x₃) is a CNF formula with three clauses over variables x₁, x₂, x₃. An assignment maps each variable to either true or false. The SAT problem asks: given a CNF formula, does there exist an assignment that satisfies all clauses simultaneously?

The general satisfiability problem can consider any Boolean formula, not necessarily in CNF, but CNF is the most common input format due to its use in resolution-based solvers. The problem is also referred to as CNF-SAT when the input is restricted to CNF.

History and significance

The study of SAT dates back to the early work of George Boole in the 19th century, but the modern computational formulation emerged in the 1960s. In 1971, Stephen Cook and independently Leonid Levin proved that SAT is NP-complete (the Cook–Levin theorem). This result established SAT as the canonical NP-complete problem, meaning that any problem in NP can be reduced to SAT in polynomial time. Consequently, if a polynomial-time algorithm for SAT exists, then P = NP, a major open question in computer science.

Despite its theoretical hardness, practical SAT solvers have made remarkable progress since the 1990s, enabling the solution of instances with millions of variables and clauses.

Algorithms

Complete solvers

Complete SAT solvers aim to either find a satisfying assignment or prove unsatisfiability. The most influential complete algorithm is the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, which performs a systematic backtracking search combined with unit propagation and pure literal elimination. Modern solvers are based on the Conflict-Driven Clause Learning (CDCL) framework, an extension of DPLL that adds non-chronological backtracking and clause learning. CDCL solvers (e.g., MiniSat, Glucose, Lingeling) are the backbone of industrial-strength SAT solving and are used in many verification and synthesis tools.

Incomplete solvers

Incomplete algorithms, such as local search (e.g., WalkSAT, GSAT) and stochastic methods, trade completeness for speed. They cannot prove unsatisfiability but often find satisfying assignments quickly on large, structured instances. These are widely used in combinatorial optimization and AI planning.

Theoretical approaches

Other approaches include resolution-based algorithms, algebraic methods (e.g., Gaussian elimination for XOR constraints), and quantum algorithms (e.g., Grover's algorithm, though not yet practical). The study of proof systems (e.g., resolution, cutting planes) is also central to understanding the complexity of SAT.

Complexity and related problems

SAT is NP-complete, meaning that no polynomial-time algorithm is known, and it is widely believed that none exists. However, many restricted variants can be solved in polynomial time, such as 2-SAT (each clause has at most two literals), Horn-SAT (clauses have at most one positive literal), and XOR-SAT (clauses are linear equations over GF(2)). The maximum satisfiability problem (MaxSAT) asks for the maximum number of clauses that can be satisfied; its decision version is NP-complete as well. #SAT (model counting) asks for the number of satisfying assignments and is #P-complete.

The Satisfiability Modulo Theories (SMT) problem extends SAT to first-order logic with theories like arithmetic, arrays, and bit vectors. Many SMT solvers (e.g., Z3, CVC5) incorporate SAT solvers as their core propositional engine.

Applications

SAT has a wide range of practical applications:

• Hardware verification: Equivalence checking, bounded model checking (BMC), and formal verification of digital circuits.
• Software verification: Bug finding, test generation, and symbolic execution (e.g., using the KLEE symbolic virtual machine).
• Artificial intelligence: Planning (SATPLAN), constraint satisfaction, automated reasoning, and diagnosis.
• Cryptography: Cryptanalysis of symmetric and public-key schemes, analysis of hash functions.
• Bioinformatics: Haplotype inference, phylogenetic tree reconstruction, and RNA folding.
• Operations research: Scheduling, resource allocation, and combinatorial optimization through encodings into MaxSAT or pseudo-Boolean constraints.

Major milestones

• 1971: Cook–Levin theorem formalizes NP-completeness of SAT.
• 1986: Introduction of the DPLL algorithm.
• 1992: GSAT and WalkSAT local search algorithms.
• 1996: Chaff solver introduces the "two-watched-literal" scheme, dramatically improving speed.
• 2001: MiniSat, a simple yet efficient CDCL solver, sparks extensive research and reuse.
• 2002: The SAT Competition series begins, driving solver performance improvements.
• 2014: Glucose and other solvers achieve high performance on industrial benchmarks.
• 2020s: SAT solvers are integrated into hardware design flows and cloud-based verification services.

See also

• Cook–Levin theorem
• Conjunctive normal form
• Satisfiability modulo theories
• Automated theorem proving
• Propositional calculus

References

• Arora, S., & Barak, B. (2009). Computational Complexity: A Modern Approach. Cambridge University Press.
• Biere, A., Heule, M., van Maaren, H., & Walsh, T. (Eds.). (2009). Handbook of Satisfiability. IOS Press.
• Cook, S. A. (1971). The complexity of theorem-proving procedures. Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 151–158.
• Gomes, C. P., Kautz, H., Sabharwal, A., & Selman, B. (2008). Satisfiability solvers. In Handbook of Knowledge Representation. Elsevier.