Satisfiability
In mathematics, a formula of propositional logic is said to be satisfiable if truth-values can be assigned to its free variables in a way that makes the formula true. The class of satisfiable propositional formulae is NP-complete, as is that of its variant 3-satisfiability. (Other variants, such as 2-satisfiability and Horn-satisfiability, can be solved by efficient algorithms.)The propositional satisfiability problem (SAT), which is given a propositional formula is to decide whether or not it is satisfiable, is of central importance in various areas of computer science, including theoretical computer science, algorithmics, artificial intelligence, hardware design and verification.
There are two classes of high-performance algorithms for solving instances of SAT in practice: modern variants of the David-Putnam-Loveland algorithm, such as zchaff, and stochastic local search algorithms, such as WalkSAT. Particularly in hardware design and verification applications, satisfiability and other logical properties of a given propositional formula are often decided based on a representation of the formula as a binary decision diagram (BDD).
Propositional satisfiability has various generalisations, including satisfiability for quantified Boolean formulae, for first- and second-order logic, constraint satisfaction problems, 0-1 integer programming, and maximum satisfiability.
Many other decision problems, such as graph colouring problems, planning problems, and scheduling problems can be rather easily encoded into SAT.
Compare with: decision problem
