In computer science, satisfiability(SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it establishes if the variables of a given Boolean formula can be assigned in such 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. For example, the formula a AND b is satisfiable because one can find the values a=TRUE and b=TRUE, which make (a AND b) = TRUE. To emphasize the binary nature of this problem, it is frequently referred to as Boolean or propositional satisfiability.
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?
- From Wikipedia