HCP to SAT Conversion Cubic Time Algorithm

HCP to SAT Conversion Cubic Time Algorithm

A byproduct of Ariadne100 development. We wrote an O(n^3) time algorithm for HCP to SAT conversion. This algorithm is actually implemented on Ariadne100 Experiment System and converts a BabaLabo format graph file to DIMACS CNF file. As far as we know this is the fastest transformation algorithm from HCP(Hamiltonian Circuit Problem) to SAT(Boolean Satisfiability Problem) ever known.

Till 1999 at least two algorithms were known for TCP→SAT conversion. One is coauthored by Iwama and Miyazaki [1] and the other is by Anatoly Plotnikov [2]. It might be said that Iwama-Miyazaki algorithm is O(nlogn) time. However this figure is not the time complexity but the number of variables in their boolean formula. They may show the existance of such a polynomial-time algorithm but never presented a concrete procedure. Consequently the efficiency remains just in theoretical possibility.

Anatoly's algorithm is quite concrete one and programmable. However in worst case, his formula has an exponential number of variables. This of course means that the algorithm is not at all of polynomial time.

We learned from Cook's proof [3] an boolean technique such as expressing a condition,

"U(x_1,...,x_i,...,x_k) is true iff exactly one x_i is true",

where U(...) is a logical function (predicate) and {x_i} is a set of k variables (literals). You will see this technique works as a very useful and strong tool for us. The detail of predicate U(…) is as shown below.

Next our tool is what we call Timing Chart. Let's consider a nxn grid system, which consists of nxn crossing points. Each column is a vertex v_i, and the lines are the time as T={1,2,...,n}. Each crossing point p_it represents the position of a vertex in time-space diagram. You can see this chart as a kind of Hasse diagram derived from the adjacency matrix of the graph. Now we can say that a graph G has a Hamiltonian cycle if and only if the following boolean relations are satisfiable.

(1)Variables are nxn crossing points p_it (and edges e_ij).
(2)In the timing chart for each v_i: exactly one p_it must be true.
(3)In the timing chart for each t: exactly one p_it must be true.
(4)If p_it and p_j[t+1] is true then the edge e_ij must exist.
(5)If p_i1 and p_jn are true, then the edge e_ji must exist.

These conditions are easily expressible by using the above predicate. As the idea is very simple and clear, I believe that we don't need any further explanation. Note: you need not to build a timing chart actually. It was just a tool for thinking. In this article, every graphs are considered to be directed. If your problem is of undirected graphs, then just replace an undirected edge with two directed multi-edges with opposite orientations.

This short article (including a pseudo C program) is mostly an excerpt from Ariadne100 Manual but slightly rewritten today for better understanding. Under lined parts are modified or added. MN(2006-09-29)

Excerpt from Ariadne100 Manual (Jun. 6, 2000)
Baba Laboratory
Michiro Nasu

HCP→SAT Polynomial Time Transformation Algorithm

NP-complete problem is a problem which is contained in NP (language) class and mutually transformable with all other NP-Complete problems in polynomial time. Cook[3,1971] proved that SAT(satisfiability problem of logical formula) is NP-complete. All of 3000 or more NP-complete problems known at present was confirmed by proving that the problem X can be transformed from SAT. On the contrary, any concrete algorithms convert problem X to SAT are scarcely (or not at all) known. All the instances proven by the time applied the same kind of abstract reasoning by Cook.

Cook showed that all of NP-Complete problems are reducible to SAT in O(P(n)^3) time by some Deterministic Turing Machine. Where P(n) is the time complexity function solving the original problem by Non-Deterministic Turing Machine. As P(n) is a polynomial function of n, the time complexity for the transformation comes to be polynomial time. From that it follows that all of NP-Complete problem can be transformed to SAT in polynomial time. However if P!=NP, can it be evidentially representable? Already 30 years have passed since Cook's proof. Where is a X→SAT (general) conversion algorithm on the earth?→see also.

Anyway, we could obtain an algorithm of O(n^3) to transform Hamiltonian Circuit Problem to SAT. The idea of the algorithm, we owes to Stanislav Busygin and his SAT01 solver. He collaborated with us to improve the efficiency of the algorithm. We decided to call it "HCP→SAT Conversion Cubic Time Algorithm". I'll give its outline now.

< HCP→ SAT Conversion Cubic Time Algorithm >

(1)Given directed graph G(V,E), n=|V|, m=|E|.

(2)Timing chart T = V*{t} = {p_it} [i=1 to n, t=1 to n].
   Hamiltonian circuit of G is a time-sequence of V on T
   like {p_v1,p_v′2,p_v′′3,…,p_(v′^n)n}, where 
   {v,v′,v′′,…,v′^n} is a permutation of 
   V={v_1,v_2,…,v_n}.

(3)Predicate U(x1,x2,…,x[k]) is true iff exactly one x[i] is true.

   U(x1, x2,…, x[k]) = (x1∨x2∨…∨x[k])
     ∧(¬x1 ∨ ¬x2)∧...∧(¬x[k-1] ∨ ¬x[k]) 
       [for all {x[i],x[j]}, i≠j, 1≤i,j≤k]

(4)Variables of the Formula: {p[it]} [i=1 to n, t=1 to n].
(5)Boolean formula: F = C1 ∧ C2 ∧ C3.

   C1 = {U(p[i1],p[i2],…,p[in])} [for all i=1 to n]
   C2 = {U(p[1t],p[2t],…,p[nt]} [for all t=1 to n]
   C3 = {¬p[it] ∨ ¬p[j(t+1)]} [if edge e(i,j) is not in E, 
           then for all i,j=1 to n. i≠j, 
                        t=1 to n, if t+1>n then t+1→1]

(6)Number of variables = n^2.
   Number of clauses = 2*n*(n^2-n+1-m/2).
   Time complexity of the algorithm = O(n^3).

[snip].

< Pseudo C code for HCP→ SAT Conversion >

#define ept(i, j) (i+(j-1)*N)
int M, N;
int AM[DMAX+1, DMAX+1];
int HCP2CNF(char *gname,  char *fname)
{
  // read graph file into adjacency matrix AM[], 
  // and get size M and order N
  ReadGraph2Mat(gname, AM, &M, &N);
  FILE *fp = fopen(fname, "w");
  if (N == 1) { // trivial graph
    fprintf(fp, "p cnf %d %d\n", 1, 1); fprintf(fp, "1 0\n");
  fclose(fp); return 1;
  }
  int i, j, k, t;
  int p=2*N*(1+N*(N-1)/2)+((N*(N-1)-M)*N); // number of clauses
  int m=N*N; // number of variable
  // print problem line
  fprintf(fp, "p cnf %d %d\n", m, p);
  // (i) C1 = PI{U(p_i1, p_i2, ... p_in)} [i=1 to n] 
  for (i=1;i<=N;i++) {
    for (t=1;t<=N;t++) fprintf(fp, "%d ", ept(i, t));
    fprintf(fp, "0\n");
    for (j=1;j<N;j++) {
      for (k=j+1;k<=N;k++) 
        fprintf(fp, "-%d -%d 0\n", ept(i, j), ept(i, k));
    }
  }
  // (ii) C2 = PI{U(p_1t, p_2t,...p_nt)} [t=1 to n]
  for (t=1;t<=N;t++) {
    for (j=1;j<=N;j++) fprintf(fp, "%d ", ept(j, t));
  fprintf(fp, "0\n");
  for (j=1;j<N;j++) {
      for (k=j+1;k<=N;k++) 
        fprintf(fp, "-%d -%d 0\n", ept(j, t), ept(k, t));
    }
  }
  //  (iii) C3 = PI{~p_it+~p_j(t+1)} [if e(i,j) is not in E]
  for (t=1;t<=N;t++) {
    for (i=1;i<=N;i++) {
      for (j=1;j<=N;j++) {
        if ((i != j) && !AM[i][j]) {
          if (t != N)  
            fprintf(fp, "-%d -%d 0\n", ept(i, t), ept(j, t+1));
          else fprintf(fp, "-%d -%d 0\n", ept(i, t), ept(j, 1));
        }
      }
    }
  }
  fclose(fp); return p;
}

< References >

[1] Iwama k., Miyazaki S, SAT-variable complexity of hard combinatorial problems, published in Proc. 13th IFIP Word Computer Congress, pp. 253-258, Hamburg, August, 1994.

[2] Anatoly Plotnikov, Designing SAT for HCP, 6th Twente Workshop on Graphs and Combinatorial Optimization Subj-class: Logic in Computer Science, 1999. http://xxx.lanl.gov/abs/cs/9903006

[3]Stephen A. Cook, The Complexity of Theorem-Proving Procedures, in Proc. of the 3rd Annual ACM Symposium on Theory of Comp. Sci., 151-158, 1971.

After Math:
■Today I realized the fact that the equality of cubic power in Cook's proof and our algorithm has a significant meaning. This is not an accidental one. In other words our algorithm is nothing but an exact and literal interpretation of Cook's formula. The reason why our Timing Chart has just n Time-steps (very short and simple) is clear. It is the length of the "Certification word" sequence. You see? So to say our Timing Chart is a very primitive (Non-Deterministic!!) Turing Machine. In this sense Cook was absolutely right and our method is said to be a template of general transformation for NP-Complete problems to SAT.

As I currently keep a temporal residence in the westward of Capitol, I have not the paper of Cook's proof at hand. I will reread the article when I return home sometime later. Perhaps you can put down a "certification word" for an NP-Complete Problem (probably) in a time-series form, and you can translate the sentence to a boolean formula by applying the predicate aforementioned. MN (2006-09-29)

■Stas(Stanislav Busygin) posted a very nice reduction from K-CLIQUE to SAT. http://tech.groups.yahoo.com/group/algorithm-forge/message/3127 Here is his answer. (2006-09-30)

Yes, the K-CLIQUE to SAT reduction is easy. Introduce K*n variables x_{ij}, i=1..K, j=1..n (where n is the number of vertices in the graph). x_{ij} is true iff vertex j is selected as i-th vertex of the clique. Then, for all i1,i2, ~x_{i1,j} OR ~x_{i2,k} if (j,k) \notin E; for all j, ~x_{ij} OR ~x_{rj}; for all i,j1!=j2, ~x_{i,j1} OR ~x_{i,j2}; for all i, x_{i1} OR x_{i2} OR ... OR x_{in}.

I responded to him:

it makes me remember that COUNTING is nothing but CORRESPONDENCE. in our terminology grid {x_{ij}} is the TIMING CHART, and K is the length of the CERTIFICATE.