next up previous contents index CD CD Algorithms
Next: Difficult Reductions Up: Satisfiability Previous: The Theory of NP-Completeness

3-Satisfiability

Satisfiability's role as the first NP-complete problem implies that the problem is hard to solve in the worst case, but certain instances of the problem are not necessarily so tough. Suppose that each clause contains exactly one literal. To satisfy such a clause, we have to appropriately set that literal, so we can repeat this argument for every clause in the problem instance. Only when we have two clauses that directly contradict each other, such as tex2html_wrap_inline26133 , will the set not be satisfiable.  

Since clause sets with only one literal per clause are easy to satisfy, we are interested in slightly larger classes. Exactly what is the clause size at which the problem turns from polynomial to hard? This transition occurs when each clause contains three literals, the so-called 3-satisfiability problem, or 3-SAT:

Input: A collection of clauses C where each clause contains exactly 3 literals, over a set of Boolean variables V.

Output: Is there a truth assignment to V such that each clause is satisfied? Since this is a more restricted problem than satisfiablity, the hardness of 3-SAT implies that satisfiability is hard. The converse isn't true, as the hardness of general satisfiability might depend upon having long clauses. We can show the hardness of 3-SAT using a reduction that translates every instance of satisfiability into an instance of 3-SAT without changing the result of whether it is satisfiable.

This reduction transforms each clause independently based on its length, by adding new Boolean variables along the way. Suppose clause tex2html_wrap_inline26135 contained k literals:

The most complicated case is that of the large clauses. If none of the original variables tex2html_wrap_inline26189 are tex2html_wrap_inline26191 , then there are not enough additional variables to be able to satisfy all of the new subclauses. You can satisfy tex2html_wrap_inline26193 by setting tex2html_wrap_inline26195 , but this forces tex2html_wrap_inline26197 , and so on until finally tex2html_wrap_inline26199 cannot be satisfied. But if any single literal tex2html_wrap_inline26201 , then we have n-3 free variables and n-3 remaining 3-clauses, so we can satisfy each of them.

This transform takes O(m+n) time if there were n clauses and m total literals in the SAT instance. Since any SAT solution also satisfies the 3-SAT instance and any 3-SAT solution sets the variables giving a SAT solution, the transformed problem is equivallent to the original.

Note that a slight modification to this construction would serve to prove that 4-SAT, 5-SAT, or any tex2html_wrap_inline26205 -SAT is also NP-complete. However, this construction breaks down when we try to use it for 2-SAT, since there is no way to stuff anything into the chain of clauses. It turns out that resolution gives a polynomial-time algorithm for 2-SAT, as discussed in Section gif.


next up previous contents index CD CD Algorithms
Next: Difficult Reductions Up: Satisfiability Previous: The Theory of NP-Completeness

Algorithms
Mon Jun 2 23:33:50 EDT 1997