Satisfiability (SAT) is the problem of determining whether there is a variable assignment that fulfills a given Boolean formula.

Satisfiability (often written in all capitals or abbreviated SAT) is the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE.

SAT was the first known example of an NP-complete problem. Further, a wide range of other naturally occurring decision and optimization problems can be transformed into instances of SAT. A class of algorithms called SAT solvers can efficiently solve a large enough subset of SAT instances to be useful in various practical areas such as circuit design and automatic theorem proving.

History of Satisfiability
Note: This is the first chapter of "Handbook of Satisfiability" (WorldCat) by Hans van Maaren, Armin Biere, Toby Walsh
Also see the timeline on page 52.

The SAT Association has Tutorials and Survey Articles

history | excerpt history