SAT is NPComplete. In fact, it was the first known NPComplete problem, as proved by Stephen Cook in 1971. The problem remains NPComplete even if all expressions are written in conjunctive normal form with 3 variables per clause (3CNF). This means the expression has the form:
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 DNFSAT and 2SAT are not NPcomplete but only that if they are then the Complexity classes P and NP are equal.
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:
We give here a sketch of the proof of NPCompleteness. To prove that SAT is NPComplete we must show that
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.
Search Encyclopedia

Featured Article
