Definition
A Propositional Logic formula, also called Boolean expression, is built from variables, operators AND, OR, NOT, and parentheses.
A formula is said to be satisfiable if it can be made TRUE by assigning appropriate logical values (i.e. TRUE, FALSE) to its variables.
The Boolean satisfiability problem (SAT) is, given a formula, to check whether it is satisfiable.
Complexity
SAT is the first known NP-complete problem