Boolean satisfiability problem

The decision problem of determining whether a Boolean formula has an assignment of truth values that makes it true. It is the canonical NP-complete problem.

Boolean formula: An expression built from Boolean variables, constants, and logical operators, with a truth value determined by its inputs. The problem asks whether at least one assignment makes such an expression true.
NP-complete problem: A decision problem in NP to which every problem in NP can be reduced in polynomial time. SAT was the first problem proved NP-complete, making it the class's defining example.
SAT solver: A program that determines whether a Boolean formula is satisfiable and may produce a satisfying assignment. Modern solvers apply search, propagation, and learning to large SAT instances.
Stephen Cook: A computer scientist whose work established the NP-completeness of Boolean satisfiability. Cook proved that every problem in NP reduces to SAT in polynomial time.
2-satisfiability: The satisfiability problem for conjunctive normal form formulas with at most two literals per clause. Unlike general SAT, 2-SAT is solvable in polynomial time.
Conjunctive normal form: A Boolean formula expressed as a conjunction of clauses, each clause being a disjunction of literals. SAT instances are often encoded in this form for algorithms and complexity proofs.
Cook–Levin theorem: The theorem that Boolean satisfiability is NP-complete. It establishes SAT's central status by encoding nondeterministic computation as a formula.
Conflict-driven clause learning: A SAT-solving technique that analyzes conflicts to derive clauses and avoid repeating failed searches. It is a defining strategy of many high-performance SAT solvers.
Leonid Levin: A mathematician and computer scientist who independently established foundational results on NP-complete problems. Levin independently proved a result equivalent to SAT's NP-completeness.
Horn satisfiability: The satisfiability problem restricted to formulas whose clauses contain at most one positive literal. This restricted SAT variant has a polynomial-time algorithm.

Linked from 16 pages