Boolean satisfiability problem

The Boolean satisfiability problem is a problem from mathematical logic. In propositional logic, a formula is satisfiable if the variables it uses can be assigned values so that the formula becomes true. Another important insight is to know that for a given formula, no such assignment exists. In other words the formula will always evaluate to false, no matter what values its variables have. In the first case, the formula is satisfiable, in the second case, it is called unsatisfiable.

The problem is also known as Boolean or propositional satisfiability. Computer scientists usually refer to it as SAT. Complexity theory usually assumes that the formula is in a special form that is known as conjunctive normal form. Formulae that are in this form have clauses, which are joined by "logical and", and that each clause has several literals, joined by "logical or". A literal and its complement cannot appear in the same clause. The problem may also have other names, which depend on what the logical formula looks like, and how many variables are used per clause.

At the beginning of the 1970s, Stephen Cook and Leonid Levin showed independently that the problem is NP-complete. This has become known as the Cook–Levin theorem.

The problem 3SAT, which uses three variables per clause, is one of the 21 NP-complete problems defined by Richard Karp in 1972.