Boolean satisfiability problem

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

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

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

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