Category:Reduction from SAT to 3CNFSAT

From LiteratePrograms
Jump to: navigation, search

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:

(x_1 \vee x_3 \vee \neg{x_4}) \wedge (\neg{x_1} \vee x_3 \vee x_5 \vee x_{10}) \wedge (x_2 \vee \neg{x_{10}})

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.