Boolean satisfiability problem

The Boolean satisfiability problem (SAT) is a decision problem considered in complexity theory. An instance of the problem is defined by a boolean expression written using only AND, OR, NOT, variables, and parentheses. The question is: given the expression, is there some assignment of TRUE and FALSE values to the variables that will make the entire expression true?

SAT is NP-Complete. In fact, it was the first known NP-Complete problem, as proved by Stephen Cook in 1971. The problem remains NP-Complete even if all expressions are written in conjunctive normal form with 3 variables per clause (3-CNF). This means the expression has the form:

(x₁₁ OR x₁₂ OR x₁₃) AND

(x₂₁ OR x₂₂ OR x₂₃) AND

(x₃₁ OR x₃₂ OR x₃₃) AND ...

where each x is a variable, with or without a NOT in front of it, and each variable can appear multiple times in the expression.

Restrictions of SAT

SAT seems to become easier if the formulas are restricted to those in disjunctive normal form, where each clause is an AND of variables (some with NOTs), and all the clauses are ORed together. This is because such a formula is satisfiable iff there is a clause which does not contain x and NOT x, and this can be checked in polynomial time. SAT also seems to be easier if the the number of literals in a clause is limited to 2, in which case the problem is called 2SAT. Also this problem can be solved in polynomial time. Note that this does not prove that DNF-SAT and 2SAT are not NP-complete but only that if they are then the Complexity classes P and NP are equal.

Extensions of SAT

The satisifiability problem seems to become more difficult if we allow quantifiers such "for all" and "there exists" that bind the boolean variables. An example of such an expression would be:

FORALL x EXISTS y EXISTS z (x OR y OR z) AND (NOT x OR NOT y OR NOT z)

In this case the the problem is called QBF (Quantified Boolean Formula) and it can be shown to be PSPACE-Complete. That is widely thought to be much harder than NP-Complete, though that has not yet been proved.

Proof of NP-completeness

We give here a sketch of the proof of NP-Completeness. To prove that SAT is NP-Complete we must show that

1. SAT is in NP, and
2. all other NP problems can be polynomially reduced to it.

First, notice that it is easy to check a YES answer: just plug in a given set of variable values, and see that they make the expression true. Therefore the problem is in NP.

Next, consider an arbitrary problem X that is in NP. By definition, there must be an algorithm for checking certificates for YES answers to X in polynomial time. Given such an algorithm it is possible to construct an (polynomial) algorithm that given the size of the certificate constructs a boolean circuit[?] that is polynomially large in the certificate size and decides wheter its input is a binary encoding of a valid certificate or not. This circuit can then be transformed by another (polynomial) algorithm into an equivalent boolean formula that is still polynomially large in the certificate size. It then holds that this formula is satisfiable iff there is a valide certificate, which means that we have reduced the original problem to SAT.