The Boolean satisfiability problem is a kind of problem in math-based logic. In propositional logic, a formula is "satisfiable" if the variables it uses can be given values so that it becomes true. If however for a given formula, no values exist so that the formula becomes true and the formula will always be false no matter what values its variables have it is called "unsatisfiable".