Reduction of Boolean Satisfiability to 3-CNF-Sat.

Let e_1 be a Boolean expression.  Assume that e_1
only uses the following operators:

not
and
or
equals
implies

(Any Boolean expression using any other operators can be easily
replaced by an equivalent expression using only the above operators.)

1.  Draw a parse tree T_1 for e_1, using an unambiguous grammar G_1 that
respects the semantics.

2.  Consider the following ambiguous grammar, G_2:

E -> E
E -> not E
E -> E or E
E -> E and E
E -> E implies E
E -> (E)
E -> V

together with several rules where V is the left-hand-side, such that
V derives any identifier.  We can use any reasonable collection of
alphanumeric strings as the identifiers, just as in programming
languages.

Convert T_1 to a parse tree T_2 of e_1 over G_2, by replacing each
internal node which is not V by E.

3.  Delete all leaves of T_2 which contain parentheses.

4.  Compress all edges where a node E has just one child which is
also E.

5.  Replace every subtree rooted at V by just a leaf labeled V.
(If a node V has a child also labeled V, the child will be deleted.)

Call the resulting tree (after executing steps 3 through 6) T_3.
Note that every leaf of T_3 is either "and," "or," "not," "implies,"
or V, while every internal node is E.  Call the resulting tree T_3.
(After steps 3 through 7.)

If a node is labeled E, and if it has only one child which is V,
we call it a "bottom" E-node.  Otherwise, we call it an
"internal" E-node.

6.  Assign an identifier to every E and every V in T_3, using the
following rules.  First, number all internal E-nodes as
E_1, E_2, ... E_m, for some m.

	a.  The identifier assigned to every V is the string
of leaves for that V in the parse tree T_1, which is one of the
identifiers of e_1.

	b.  The identifier of a bottom E-node is the identifier
of its child.

	c.  We assume we have a string generator that generates
all possible identifiers in canonical order.  We assign an
identifier to each internal E-node in sequence.  For each i
from 1 to m, assign E_i the first identifier that has not
been previously assigned to any node.  We call the identifiers
assigned to the E_i "dummies."

7.  For each internal E-node, E_i, we create one clause, f_i, as
follows.  Let x_i be the identifier of E_i.

	a.  If the children of E_i are "not" and E', let x' be
the identifier of E'.  Then f_i is
		x_i = !x'

	b.  If the children of E_i are E', "equals" and E", let x',
x" be the identifiers of E', E", respectively.  Then f_i is
		x_i = (x' = x")

	c.  If the children of E_i are E', "or" and E", let x',
x" be the identifiers of E', E", respectively.  Then f_i is
		x_i = (x' + x")

	d.  If the children of E_i are E', "and" and E", let x',
x" be the identifiers of E', E", respectively.  Then f_i is
		x_i = (x' * x")

	e.  If the children of E_i are E', "implies" and E", let x',
x" be the identifiers of E', E", respectively.  Then f_i is
		x_i = (x' => x")

Convert each f_i into a 3-CNF expression <f_i>, as given by the table
above.  Let e_2 = <f_1><f_2> ... <f_m>, which is a 3-CNF expression.

Theorem 1.  If |e_1| = n, then |e_2| = O(n log n), and the amount
of time needed to construct e_2 from e_1 is a polynomial function of n.

Theorem 2: e_1 is satisfiable if and only if e_2 is satisfiable.

Theorems 1 and 2 mean that, by definition, we have a reduction of
Boolean satisfiability to 3-CNF-Sat.