
This page introduces an NPcomplete problem based on propositional logic.
A literal is a either a propositional variable or the negation of a propositional variable.
Variables, such as x and y, are called positive literals.
Negated variables, such as ¬x and ¬y, are called negative literals.
A clause is a disjunction (or) of one or more literals. For example,
is a clause.
A clausal formula, which we will just call a formula, is a conjunction (and) of one or more clauses.
For example,
(¬x ∨ y) ∧ 
(¬y ∨ z) ∧ 
(x ∨ ¬z ∨ y) 
is a (clausal) formula.
Definition. A formula φ is satisfiable if there exists an assignment of values to its variables that makes φ true.
For example, formula
(¬x ∨ y) ∧ 
(¬y ∨ z) ∧ 
(x ∨ ¬z ∨ y) 
is satisfiable. Choose
x = false 
y = true 
z = true 
The satisfiability problem, usually called SAT, is the following language.
Thought of as a computational problem, the input to SAT is a clausal formula φ and the problem is to determine whether φ is satisfiable.
Cook and Levin independently proved that SAT is NPcomplete.
(Both did so before the term NPcomplete was even in use. Their work led to the study of NP.)
Cook/Levin Theorem. SAT is NPcomplete.
Proof. There are two parts to the proof because there are two parts to the definition of NPcompleteness.
First, you must show that SAT is in NP.
Then you must show that, for every problem X in NP, X ≤_{p} SAT.
The first part is by far the easiest. The satisfiablity problem can be expressed as a test for existence.
φ is satisfiable ⇔ there exists an assignment A of truth values to the variables in φ so that assignment A makes φ true.
So a nondeterministic algorithm for SAT goes like this.
Evidence for φ. An assignment of truth values to the variables that occur in φ.
The evidence is accepted if: the assignment makes φ true.
The second part (X ≤_{p} SAT for every X in NP) is considerably more difficult.
The proof is by a quite long generic reduction. Sipser describes the entire proof.
I do not duplicate the proof here, but here is a very rough sketch of how it goes.
Given an arbitrary language X in NP, select a polynomialtime nondeterministic Turing machine M for X.
Since M runs in polynomial time, there must be a k so that M runs in time n^{k}.
To show that X ≤_{m} SAT, we need a polynomialtime computable function f so that, for every y,
Suppose that y has length n.
Notice that f(y) produces a clausal formula.
f(y) begins by creating propositional variables e_{1} … e_{z} where z = n^{k}.
Since M only runs for n^{k} steps on input y, M cannot look at more bits of evidence than that.
f(y) writes down a logical (clausal) formula φ that expresses, in logic,
"M accepts input (y, e) where e = e_{1}…e_{z}."
Formula φ does not say anything directly about the evidence variables. But once they are chosen, the remaining variables are constrained to describe a computation of M on input (y, e).
So φ is satisfiable if and only if there exist values of the evidence variables so that M accepts input (y, e). But, by the choice of M, that is equivalent to saying that y ∈ X. ◊
It should not come as a great surprise that you can use logic to describe computation. After all, computers are built from logic gates, such as andgates, orgates and notgates (inverters).
First, the Cook/Levin theorem tells us that, if the conjecture that P ≠ NP is correct, then SAT is not in P.
It also makes it unnecessary to do more generic reductions in proofs of NPcompleteness.
Suppose that you want to show that some language, W, is NPcomplete.
First, of course, you show that W is in NP. So you find a polynomialtime nondeterministic algorithm for W.
Then you must show that X <_{p} W for every X in NP.
But that can be done by showing that SAT ≤_{p} W.
Then, since X ≤_{p} SAT and SAT ≤_{p} W, X ≤_{p} W, for every X in NP.
