# Category:Reduction from SAT to 3CNFSAT

One of the first problems to be shown NP-complete was the [boolean satisfiability problem] (**SAT**). A surprising fact is that we do not need the full generality of boolean formulas to achieve this hardness result; it suffices to consider formulas that are both in conjunctive normal form (**CNF**). In conjunctive normal form these properties hold:

- All negations (NOTs) are applied directly to input variables. A variable or its negation is referred to as a
*literal*. - The formula is a conjunction (AND) of
*clauses*, where each clause is a disjunction (OR) of literals.

A simple example might be:

Moreover, we can limit ourselves to formulas where every clause contains only three literals, like the first clause above. This is called 3CNF form, and the satisfiability problem for it is called **3CNFSAT**. We will give an efficient polynomial-time algorithm that converts any boolean formula to a 3CNF formula that is satisfiable if and only if the original formula is (the definition of a many-one reduction).

*This category currently contains no pages or media.*