Wednesday, 12 June 2013

Foundations of Complexity Lesson 13: Satisfiability

Boolean-Formula Satisfiability (SAT) is the single most important language in computational complexity. Here is an example of a Boolean formula.

(u OR v) AND (u OR v) 
u and v are variables that take on values from {TRUE, FALSE}. u means the negation of u. A literal is either a variable or its negation.

An assignment is a setting of the variables to true and false, for example (u→TRUE, v→FALSE). Once all of the variables are assigned a truth value, the formula itself has a truth value. The assignment (u→TRUE, v→FALSE) makes the formula above false. A satisfying assignment is an assignment that makes the formula true. For the formula above, the assignment (u→TRUE, v→TRUE) is satisfying. If a formula has a satisfying assignment we say the formula is satisfiable.

SAT is the set of satisfiable formula. The formula above is in SAT. This formula is not.

u AND (u OR v) AND (u or v
A formula is in conjunctive normal form (CNF) if it is the AND of several clauses, each consisting of an OR of literals, like the formulas above. A disjunctive normal form (DNF) formula is the same with AND and OR reversed. A formula is k-CNF if every clause has exactly k literals. The first formula above is in 2-CNF.

CNF-SAT is the set of satisfiable CNF formulas. k-CNF-SAT or k-SAT is the set of satisfiable formulas in k-CNF.

Cook and Levin independently showed that SAT is NP-complete. The problem remains NP-complete if we restrict to CNF-SAT or even 3-SAT.

Next lesson we will show that CNF-SAT is NP-complete.