Boolean satisfiability problem

related topics
{math, number, function}
{theory, work, human}
{day, year, event}
{system, computer, user}
{work, book, publish}
{game, team, player}

Satisfiability 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. Equally important is to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically FALSE for all possible variable assignments. In this latter case, we would say that the function is unsatisfiable; otherwise it is satisfiable. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability. The shorthand "SAT" is also commonly used to denote it, with the implicit understanding that the function and its variables are all binary-valued.


Basic definitions, terminology and applications

In complexity theory, the satisfiability problem (SAT) is a decision problem, whose instance is a Boolean expression written using only AND, OR, NOT, variables, and parentheses. The question is: given the expression, is there some assignment of TRUE and FALSE values to the variables that will make the entire expression true? A formula of propositional logic is said to be satisfiable if logical values can be assigned to its variables in a way that makes the formula true. The Boolean satisfiability problem is NP-complete. The propositional satisfiability problem (PSAT), which decides whether a given propositional formula is satisfiable, is of central importance in various areas of computer science, including theoretical computer science, algorithmics, artificial intelligence, hardware design, electronic design automation, and verification.

Full article ▸

related documents
Direct sum of modules
Integration by parts
Riemann zeta function
Newton's method
Series (mathematics)
Principal components analysis
List of trigonometric identities
Johnston diagram
Forcing (mathematics)
Stone–Čech compactification
Pascal's triangle
Russell's paradox
Cauchy sequence
Complete lattice
Bra-ket notation
Ruby (programming language)
Mathematical induction
Denotational semantics
Non-standard analysis
Numerical analysis
Kernel (algebra)
Cardinal number
Sequence alignment
Gaussian elimination
Entropy (information theory)
Logic programming