Guest User

Untitled

a guest
Feb 13th, 2014
55
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. #include <stp/c_interface.h>
  2. #include <vector>
  3. #include <iostream>
  4. #include <sstream>
  5. #include <string>
  6. #include <stdlib.h>
  7.  
  8. using namespace std;
  9.  
  10. int main(int argc, char** argv) {
  11.     int colors = 3;
  12.     int n = 0;
  13.  
  14.     if(argc <= 1) {
  15.         cout << "Usage: " << argv[0] << " n" << endl;
  16.         exit(1);
  17.     }
  18.     else {
  19.         n = atoi(argv[1]);
  20.     }  
  21.  
  22.     VC handle = vc_createValidityChecker();
  23.  
  24.     //create binary variable of length "colors" for each vertex
  25.     cout << "Stage 1: Generating variables for each vertex" << endl;
  26.     std::vector<Expr> color_map;   
  27.     for (int i = 0; i < n; ++i) {
  28.         for (int j = 0; j <= i; ++j) {
  29.             stringstream name;
  30.             name << "col_" << i+1 << "_" << j+1;
  31.             string name_st = name.str();
  32.  
  33.             Expr x = vc_varExpr(handle, name_st.c_str(), vc_bvType(handle, colors));
  34.             color_map.push_back(x);
  35.         }
  36.     }
  37.  
  38.     //now we generate inequalities 
  39.     cout << "Stage 2: Generating basic inequalities" << endl;
  40.     for (int i = 0; i < n; ++i) {
  41.         for (int j = 0; j <= i; ++j) {
  42.             int index = i*(i + 1)/2+j;
  43.             Expr cond = NULL;
  44.             std::vector<Expr> feasibility;
  45.  
  46.             //every vertex gets exactly one        
  47.             for(int k = 0; k < colors; ++k) {
  48.                 Expr result = NULL;
  49.                 for(int l = 0; l < colors; ++l) {
  50.                     Expr is_color_l = vc_notExpr(handle,vc_bvBoolExtract_One(handle,color_map[index],l));
  51.                     if(l == k) {
  52.                         is_color_l = vc_notExpr(handle,is_color_l);
  53.                     }
  54.                     if(result == NULL) {
  55.                         result = is_color_l;
  56.                     }
  57.                     else {
  58.                         result = vc_andExpr(handle,result,is_color_l);
  59.                     }
  60.                 }
  61.  
  62.                 feasibility.push_back(result);
  63.             }
  64.  
  65.             vc_assertFormula(handle,vc_orExprN(handle,&feasibility[0],feasibility.size()));
  66.         }
  67.     }
  68.  
  69.     //no triangle has uniform colors
  70.     cout << "Stage 3: Generating coloring inequalities" << endl;
  71.     for (int i = 0; i < n; ++i) {
  72.         for (int j = 0; j <= i; ++j) {
  73.             //(i,j) is the tip
  74.             for( int i2 = i+1; i2 < n; ++i2) {
  75.                 int j2 = j;
  76.                 int j3 = j2+(i2-i);
  77.                 if(j3 > i2) continue;
  78.  
  79.                 //we now consider the triangle (i,j) (i2,j2) (i2,j3)
  80.                 int v = i *(i  + 1)/2+j ;
  81.                 int w = i2*(i2 + 1)/2+j2;
  82.                 int q = i2*(i2 + 1)/2+j3;
  83.  
  84.                 //v w and q do not all have the same color             
  85.                 for(int k = 0; k < colors; ++k) {                  
  86.                     Expr has_v_col_k = vc_bvBoolExtract_One(handle,color_map[v],k); //extract bit k
  87.                     Expr has_w_col_k = vc_bvBoolExtract_One(handle,color_map[w],k);
  88.                     Expr has_q_col_k = vc_bvBoolExtract_One(handle,color_map[q],k);
  89.  
  90.                     //if v and w have the same color, q has a different color, etc
  91.                     Expr cond_vw = vc_impliesExpr(handle,vc_andExpr(handle,has_v_col_k,has_w_col_k),vc_notExpr(handle,vc_andExpr(handle,has_v_col_k,has_q_col_k)));
  92.  
  93.                     vc_assertFormula(handle,cond_vw);
  94.                 }              
  95.             }
  96.         }
  97.     }
  98.  
  99.     cout << "Stage 4: Solving" << endl;
  100.     int result = vc_query(handle,vc_falseExpr(handle)); //find counterexample
  101.     switch(result)  {
  102.     case 0:
  103.         cout << "Found a valid coloring with " << colors << " colors for n=" << n << endl;
  104.         vc_printCounterExample(handle);
  105.         break;     
  106.     case 1:
  107.         cout << "Could NOT find a coloring with " << colors << " colors for n=" << n << endl;      
  108.         break;
  109.     default:
  110.         cout << "Unexpected result from vc_query (" << result << ")" << endl;
  111.     }
  112.  
  113.     //clean up
  114.     vc_Destroy(handle);
  115.     color_map.clear();
  116.  
  117.     return 0;
  118. }
RAW Paste Data