We define L_bool to be the set of all boolean expressions. It really doesn't matter how we define "boolean expression," any consistent definition will do. For example, we could define it to mean any expression of boolean type in the Pascal programming language, given that all identifiers are variables of boolean type, and no functions are allowed. You could use C++, or whatever suits your fancy instead.

Just to be definite, we'll define a boolean expression as follows.

1. The alphabet consists of all lower case roman letters and the digits, together with the symbols (,),+,*,~,=,<.
2. Any identifier consists of any string of letter and digits starting with a letter.
3. "+" stands for "or," "*" stands for "and," and "~" stands for "not."
4. "=" stands for "equals" (i.e., same boolean value) and "<" stands for "implies." (I know that a right arrow is usually used for "implies", but I want to have just one symbol.)
5. The precedence of the operators is that "not" has higher precedence than "and" which has higher precedence than "or", which has higher precedence than "implies," which has higher precedence than "equals". Since "implies" is not associative, we shall use the usual left-first rule, that is, x
6. Parentheses are used in the usual way.

We refer to the action of the "and" operator as conjunction. We refer to the action of the "or" operator as disjunction. We refer to the action of the "not" operator as negation.

We didn't really need "equals" and "implies," but they make the proof that boolean satisfiability is NP-complete easier.

Note that L_bool is a context-free language, and is therefore in the class P.

A boolean expression is satisfiable if there is an assignment of boolean values to the variables which causes the expression to be evaluated as true. A boolean expression is a contradiction if and only if it is not satisfiable.

Let L_sat be the language of all satisfiable boolean expressions.

Theorem 1. L_sat is NP-complete.

Theorem 1 must be proved by hand, as it were. We'll postpone that.

A boolean expression is said to be in conjunctive normal form (or CNF) if it is the conjunction of a number of clauses, where each clause is the disjunction o a number of terms, where each term is either a variable or the negation of a variable.

A boolean expression is said to be 3-CNF if it is CNF, and if each clause has exactly 3 terms.

Let L_3-cnf be the language of all 3-CNF boolean expressions, also a context-free language.

Let L_3-cnf-sat be the language of all satisfiable 3-CNF boolean expressions. Note that L_3-cnf-sat is the intersection of L_3-cnf and L_sat.

Theorem 2. L_3-cnf-sat is NP-complete.

Trivially, L_3-cnf-sat is NP. We prove Theorem 2 from Theorem 1 by giving a polynomial time reduction from L_sat to L_3-cnf-sat. We do this by constructing a reduction F such that:

• If w in L_bool, then F(w) in L_3-cnf, and w is satisfiable if and only if F(w) is satisfiable.
• If w is not in L_bool, then F(w) is some nonsense string.
• It takes polynomial time to compute F(w).