Reductions To SAT

Standa Zivny asks

I'd like to ask you about CLIQUE→SAT reduction. The reduction 3-SAT→CLIQUE is a standard one from undergrad course. Since SAT is NP-Complete, every problem from NP, i.e., CLIQUE as well, is reducible to SAT. Is this reduction "known", i.e. defined by some "natural way" as the reduction 3-SAT→CLIQUE is? Is that true for all NP-C problems?

The reduction in Cook's paper create formulas with variables that represent the entire computation of an NP machine accepting CLIQUE. We can often do much better. Consider the problem of determining whether a graph on n vertices has a clique of size k.

Variables: y_i,r (true if node i is the rth node of the clique) for 1 ≤ i ≤ n, 1 ≤ r ≤ k.

Clauses:

• For each r, y_1,r∨y_2,r∨…∨y_n,r (some node is the rth node of the clique).
• For each i, r<s, ¬y_i,r∨¬y_i,s (no node is both the rth and sth node of the clique).
• For each r≠s and i<j such that (i,j) is not an edge of G, ¬y_i,r∨¬y_j,s. (If there's no edge from i to j then nodes i and j cannot both be in the clique).

That's the entire formula that will be satisfiable if and only if G has a clique of size k.

While simple, an optimized Cook-Levin style reduction can produce smaller formula for large k. This reduction has Θ(n²k²) clauses. Using Robson's reduction one can create formulas of size O(n²log^O(1)n).

We can get similarly nice reductions for many other NP-complete problems like 3-COLORING and HAMILTONIAN CYCLE. But there is no general procedure for producing simple formula, especially if there are calculations involved like SUBSET SUM.