
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 binaryvalued.
Contents
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 NPcomplete. 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 
Functor 
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 
Groupoid 
Infinity 
Complete lattice 
Braket notation 
Ruby (programming language) 
Mathematical induction 
Denotational semantics 
Nonstandard analysis 
Numerical analysis 
Kernel (algebra) 
Cardinal number 
Sequence alignment 
Gaussian elimination 
Addition 
Entropy (information theory) 
Logic programming 
