Boolean satisfiability, L_sat, is NP-complete.

Boolean satisfiability is trivially NP.  We need to prove the following:

Given any NP language L, there is a polynomial time reduction of L to L_sat.

Suppose that M is a NTM that accepts L in polynomial time.  That is,
there is some k such that, if w in L, and if |w| = n, then there is
a valid computation of M with input w, of length at most n^k.

We construct a program P that takes as input a string w,
and gives as output a boolean expression e_w, such that
	a) e_w is satisfiable if and only if there exists a valid
	computation of M with input w of length at most n^k.
	b) the amount of time it takes P to execute is O(n^{2k}).

We first note that a valid computation of M with n^k steps can be
written as a string v with at most n^{2k} symbols.  The reason is that
the valid computation is the concatenation of n^k configurations, and
each configuration can be written as a string of length at most n^k.
(Do you see why?)

Suppose that the number of symbols in the alphabet of computations is m,
which is a constant (i.e., it does not depend on n).  Then e_w will have
approximately n^{2k}m variables.  For each symbol a and each integer
t in the range 1..n^{2k}, there is a variable which represents the
statement, "The t-th symbol of v is a."  A given concatenation v of
configurations then induces an assignment of those variables.  We
need to design e_w in such a way that this assignment is a satisfying
assignment for e_w if and only if v is a valid computation.

The way we do that is ... [to be continued]