CNF Satisfiability Problem is NP-Complete

== Theorem ==
The conjunctive normal form boolean satisfiability problem (CNF SAT) is NP-complete.
== Proof ==
Let $P$ be a CNF SAT problem.
=== CNF SAT is NP ===
A potential solution to $P$ can be verified in polynomial time by checking every clause in $L$ to see if they all have at least one true un-negated variable or one false negated variable.
Because a solution can be verified or rejected in polynomial time the problem is NP
=== CNF SAT is NP-hard ===
We will show this by reducing the boolean satisfiability (SAT) problem to CNF SAT.
The algorithm to convert the SAT) problem to CNF SAT is recursive.
Wherever $A$, $B$,and $C$ are seen in the output it is understood that the algorithm would call itself on those formulas and convert them into CNF.
==== iff and xor ====
The first step will be to remove every instance of mutual implication and exclusive or from the problem.
In every clause with one of these functions there must be at least one that does not have any instance of mutual implication or exclusive or in its arguments.
Introduce a new variable $x$ and replace either:
:$A \implies B$ with $x$
or:
:$\map \neg {A \implies B}$ with $\neg x$
as appropriate.
Then add the following four clauses to $L$:
:$A \lor B \lor x$
:$A \lor \neg B \lor \neg x$
:$\neg A \lor B \lor \neg x$
:$\neg A \lor \neg B \lor x$
Repeat this procedure until there are no more mutual implications or exclusive ors in the list of clauses.
It is important to note that the amount this procedure adds to the size of the final problem is bounded.
Specifically, every instance of mutual implication or exclusive or increases the number of variables by one, increases the number of "new" symbols in $L$ by a fixed number and reproduces every "old" symbol in $L$ at most four times.
In total, this step increases the size of the problem at most linearly.
The remaining functions that need to be considered can be converted to CNF with only a constant amount of increase to the size by a constant amount per production.
Given a logical expression it will either be a variable, a unary function, or a binary function.
==== Single Variable ====
If $A$ is a single variable then it is in CNF and the task is complete.
==== Unary functions ====
With the two constant functions, one can simply replace $\map {f_\F} A$ and $\map {f_\T} A$ with $\F$ and $\T$ respectively.
These can then be removed from the final expression as appropriate.
For the identity function, replace $\map {f_I} A$ with the CNF conversion of $A$.
With the $\neg$ function the replacement depends on the argument.
If the argument is a single variable $x$ then the output $\neg x$ is in CNF.
If the argument is one of the constant functions then replace $\neg \map {f_\F} A$ and $\neg \map {f_\T} A$ with $\T$ and $\F$ respectively.
If the argument is a binary function of the form $\map f {A, B}$ then replace the function with the appropriate one, following the list below:
:$\neg \map {f_\F} {A, B} \to \map {f_\T} {A, B}$
:$\neg \map {f_\T} {A, B} \to \map {f_\F} {A, B}$
:$\neg A \land B \to A \uparrow B$
:$\neg A \uparrow B \to A \land B$
:$\map \neg {A \implies B} \to \map \neg {A \implies B}$
:$\map {\neg \neg} {A \implies B} \to \paren {A \implies B}$
:$\neg \map {\pr_1} {A, B} \to \map {\overline {\pr_1} } {A, B}$
:$\neg \map {\overline {\pr_1} } {A, B} \to \map {\pr_1} {A, B}$
:$\neg \left({B \implies A}\right) \to \neg \left({B \implies A}\right)$
:$\neg \neg \left({B \implies A}\right) \to \left({B \implies A}\right)$
:$\neg \pr_2 \to \overline {\pr_2}$
:$\neg \overline {\pr_2} \to \pr_2$
:$\neg A \lor B \to A \downarrow B$
:$\neg A \downarrow B \to A \lor B$
==== Binary Functions ====
Replace $\map {f_\T} {A, B}$ with $\T$.
$A \lor B$ is already in CNF.
Replace $A \implies B$ with $\neg A \lor B$.
Replace $\map {\pr_1} {A, B}$ with $A$.
Replace $B \implies A$ with $A \lor \neg B$.
Replace $\map {\pr_2} {A, B}$ with $B$.
In the case of $A \land B$ the clause takes either the form:
:$A \land B$
or:
:$\paren {A \land B} \lor C$
In the first case simply replace the clause with the two clauses $A$ and $B$.
In the second case introduce the new variable $x$ and replace the clause with the three clauses:
:$x \lor C$
:$\neg x \lor A$
:$\neg x \lor B$
A simple case analysis will show that the above clauses have a solution $\paren {A \land B} \lor C$.
Replace $A \uparrow B$ with $\neg A \lor \neg B$
 
Replace $\map {\overline {\pr_2} } {A, B}$ with $\neg B$.
Replace $\map \neg {A \implies B}$ with $A \land \neg B$ and use the rule for $A \land B$.
Replace $\map {\overline {\pr_2} } {A, B}$ with $\neg A$.
Replace $\map \neg {B \implies A}$ with $\neg A \land B$ and use the rule for $A \land B$.
Replace $A \downarrow B$ with $\neg A \land \neg B$ and use the rule for $A \land B$.
Replace $\map {f_\F} {A, B}$ with $\F$.
At this point there may be some instances of $\T$ and $\F$ in the clauses.
They can be removed by:
:deleting any clause from $L$ that contains $\T$ in any of its conjunctions
and:
:removing $\F$ from any clause that contains it.
Note that if any clause simplifies to $\F$ the problem is trivially unsatisfiable and the task is complete.
In the end the size and number of variables in the CNF problem is $\map \OO n$ where $n$ is the number of symbols required to write down the original SAT problem.
Hence the conversion can be done in polynomial time.
We have that Boolean Satisfiability Problem is NP-hard.
But SAT is reducible to CNF SAT.
Therefore CNF SAT is NP-hard.
CNF SAT is NP-complete.
Category:Mathematical Logic