Sunday, December 10, 2006

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: yi,r (true if node i is the rth node of the clique) for 1 ≤ i ≤ n, 1 ≤ r ≤ k.

Clauses:

  • For each r, y1,r∨y2,r∨…∨yn,r (some node is the rth node of the clique).
  • For each i, r<s, ¬yi,r∨¬yi,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, ¬yi,r∨¬yj,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 Θ(n2k2) clauses. Using Robson's reduction one can create formulas of size O(n2logO(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.

3 comments:

  1. pls help how to transform boolean data table to SAT, I need to use minsat to minimize boolean data table, thank you very much in advance

    ReplyDelete
  2. is this good
    http://minisat.se/SatELite.html
    SatELite is a CNF minimizer, intended to be used as a preprocessor to the SAT solver. It is designed to compress the CNF fast enough not to be a bottle neck, and is particularly aimed at improving SAT encodings resulting from translation of netlists (combinational boolean circuits).

    ReplyDelete
  3. Nice reduction! similar to maximum colorful clique.

    ReplyDelete