replace ckvec with map in satisfiability program
authorYanhua YanhuaSunLaptop <yanhuasun@yanhua-suns-macbook-pro.local>
Sun, 4 Apr 2010 05:40:01 +0000 (00:40 -0500)
committerYanhua YanhuaSunLaptop <yanhuasun@yanhua-suns-macbook-pro.local>
Sun, 4 Apr 2010 05:40:01 +0000 (00:40 -0500)
examples/charm++/satisfiability/main.C
examples/charm++/satisfiability/par_Solver.C
examples/charm++/satisfiability/par_Solver.h

index 86a49103896c8a1bf79d9f2a2ce8de369c64d3fa..68d459b023009f5a3e3f5e0f997f8a29f42093d5 100644 (file)
@@ -27,6 +27,8 @@ using namespace std;
 
 //#include "util.h"
 
+typedef map<int, int> map_int_int;
+
 CProxy_Main mainProxy;
 
 #define CHUNK_LIMIT 1048576
@@ -140,13 +142,13 @@ static void simplify(par_SolverState& S)
            pp_j_ = 2;
        }
        S.occurrence[pp_*toInt(lit)-1] = -pp_i_;
-       CkVec<int> &inClauses = S.whichClauses[pp_*2*toInt(lit)-pp_i_];
-       CkVec<int> &inClauses_opposite = S.whichClauses[pp_*2*toInt(lit)-pp_j_];
+       map_int_int &inClauses = S.whichClauses[pp_*2*toInt(lit)-pp_i_];
+       map_int_int &inClauses_opposite = S.whichClauses[pp_*2*toInt(lit)-pp_j_];
        
        // literal with same sign
-       for(int j=0; j<inClauses.size(); j++)
+       for( map_int_int::iterator iter = inClauses.begin(); iter!=inClauses.end(); iter++)
        {
-           int cl_index = inClauses[j];
+           int cl_index = (*iter).first;
 #ifdef DEBUG
            CkPrintf(" %d \n \t \t literals in this clauses: ", cl_index);
 #endif
@@ -164,37 +166,22 @@ static void simplify(par_SolverState& S)
                if(toInt(lit_) > 0)
                {
                    S.positive_occurrence[toInt(lit_)-1]--;
-                   //S.whichClauses[2*toInt(lit_)-2].remove(cl_index);
-                //remove the clause index for the literal
-                    /* Low effieciency */
-                   for(int _i = 0; _i<S.whichClauses[2*toInt(lit_)-2].size(); _i++)
-                   {
-                       if(S.whichClauses[2*toInt(lit_)-2][_i] == cl_index)
-                       {
-                           S.whichClauses[2*toInt(lit_)-2].remove(_i);
-                            break;
-                       }
-                   }
-
+                   map_int_int::iterator one_it = S.whichClauses[2*toInt(lit_)-2].find(cl_index);
+                   S.whichClauses[2*toInt(lit_)-2].erase(one_it);
                }else
                {
-                   for(int _i = 0; _i<S.whichClauses[-2*toInt(lit_)-1].size(); _i++)
-                   {
-                       if(S.whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
-                       {
-                           S.whichClauses[-2*toInt(lit_)-1].remove(_i);
-                           break;
-                       }
-                   }
+                   map_int_int::iterator one_it = S.whichClauses[-2*toInt(lit_)-1].find(cl_index);
+                   S.whichClauses[-2*toInt(lit_)-1].erase(one_it);
                }
+
            }
            
            S.clauses[cl_index].resize(0); //this clause goes away. In order to keep index unchanged, resize it as 0
        }
        
-       for(int j=0; j<inClauses_opposite.size(); j++)
+       for(map_int_int::iterator iter= inClauses_opposite.begin(); iter!=inClauses_opposite.end(); iter++)
        {
-           int cl_index_ = inClauses_opposite[j];
+           int cl_index_ = (*iter).first;
            par_Clause& cl_neg = S.clauses[cl_index_];
            cl_neg.remove(-toInt(lit));
            //becomes a unit clause
@@ -402,7 +389,6 @@ void Main::done(CkVec<int> assignment)
     CkPrintf("\nFile reading and processing time:         %f\n", readfiletimer-starttimer);
     CkPrintf("Solving time:                             %f\n", endtimer - readfiletimer);
  
-    /*
     FILE *file;
     char outputfile[50];
     sprintf(outputfile, "%s.sat", inputfile);
@@ -412,7 +398,6 @@ void Main::done(CkVec<int> assignment)
     {
         fprintf(file, "%d\n", assignment[i]);
     }
-    */
     CkExit();
 }
 #include "main.def.h"
index 22a472f6b72bddcd69e51b209e232f6e07d0c4f3..975afb9c347cde7aa4606aceefecaa2de47d3167 100644 (file)
@@ -108,9 +108,9 @@ bool par_SolverState::addClause(CkVec<par_Lit>& ps)
         par_Lit lit = ps[i];
 
         if(toInt(lit) > 0)
-            whichClauses[2*toInt(lit)-2].push_back(clauses.size()-1);
+            whichClauses[2*toInt(lit)-2].insert(pair<int, int>(clauses.size()-1, 1));
         else
-            whichClauses[-2*toInt(lit)-1].push_back(clauses.size()-1);
+            whichClauses[-2*toInt(lit)-1].insert(pair<int, int> (clauses.size()-1, 1));
 
     }
 
@@ -156,15 +156,14 @@ mySolver::mySolver(par_SolverState* state_msg)
 
         next_state->occurrence[pp_*toInt(lit)-1] = -pp_i_;
     
-        //CkPrintf(" index=%d, total size=%d, original msg size=%d\n", pp_*2*toInt(lit)-pp_i_, next_state->whichClauses.size(), state_msg->whichClauses.size());
 
-        CkVec<int> &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
-        CkVec<int> &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
+        map_int_int &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
+        map_int_int  &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
 
     // literal with same sign, remove all these clauses
-       for(int j=0; j<inClauses.size(); j++)
+       for( map_int_int::iterator iter = inClauses.begin(); iter!=inClauses.end(); iter++)
        {
-           int cl_index = inClauses[j];
+           int cl_index = (*iter).first;
 
            par_Clause& cl_ = next_state->clauses[cl_index];
            //for all the literals in this clauses, the occurrence decreases by 1
@@ -177,33 +176,21 @@ mySolver::mySolver(par_SolverState* state_msg)
                if(toInt(lit_) > 0)
                {
                    next_state->positive_occurrence[toInt(lit_)-1]--;
-                   //remove the clause index for the literal
-                   for(int _i = 0; _i<next_state->whichClauses[2*toInt(lit_)-2].size(); _i++)
-                   {
-                       if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
-                       {
-                           next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
-                           break;
-                       }
-                   }
+                   map_int_int::iterator one_it = next_state->whichClauses[2*toInt(lit_)-2].find(cl_index);
+                   next_state->whichClauses[2*toInt(lit_)-2].erase(one_it);
                }else
                {
-                   for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
-                   {
-                       if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
-                       {
-                           next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
-                           break;
-                       }
-                   }
+                   map_int_int::iterator one_it = next_state->whichClauses[-2*toInt(lit_)-1].find(cl_index);
+                   next_state->whichClauses[-2*toInt(lit_)-1].erase(one_it);
                }
+               
            } //finish dealing with all literal in the clause
            next_state->clauses[cl_index].resize(0);
        } //finish dealing with clauses where the literal occur the same
        /* opposite to the literal */
-       for(int j=0; j<inClauses_opposite.size(); j++)
+       for(map_int_int::iterator iter= inClauses_opposite.begin(); iter!=inClauses_opposite.end(); iter++)
        {
-           int cl_index_ = inClauses_opposite[j];
+           int cl_index_ = (*iter).first;
            par_Clause& cl_neg = next_state->clauses[cl_index_];
            cl_neg.remove(-toInt(lit));
 
@@ -398,14 +385,14 @@ bool mySolver::seq_solve(par_SolverState* state_msg)
 
     next_state->occurrence[pp_*toInt(lit)-1] = -pp_i_;
     
-    CkVec<int> &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
-    CkVec<int> &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
+    map_int_int &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
+    map_int_int &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
 
     // literal with same sign, remove all these clauses
-    for(int j=0; j<inClauses.size(); j++)
+    
+    for( map_int_int::iterator iter = inClauses.begin(); iter!=inClauses.end(); iter++)
     {
-        int cl_index = inClauses[j];
-
+        int cl_index = (*iter).first;
         par_Clause& cl_ = next_state->clauses[cl_index];
         //for all the literals in this clauses, the occurrence decreases by 1
         for(int k=0; k< cl_.size(); k++)
@@ -417,33 +404,21 @@ bool mySolver::seq_solve(par_SolverState* state_msg)
             if(toInt(lit_) > 0)
             {
                 next_state->positive_occurrence[toInt(lit_)-1]--;
-                //remove the clause index for the literal
-                for(int _i = 0; _i<next_state->whichClauses[2*toInt(lit_)-2].size(); _i++)
-                {
-                    if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
-                    {
-                        next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
-                        break;
-                    }
-                }
+                map_int_int::iterator one_it = next_state->whichClauses[2*toInt(lit_)-2].find(cl_index);
+                next_state->whichClauses[2*toInt(lit_)-2].erase(one_it);
             }else
             {
-                for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
-                {
-                    if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
-                    {
-                        next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
-                        break;
-                    }
-                }
+                map_int_int::iterator one_it = next_state->whichClauses[-2*toInt(lit_)-1].find(cl_index);
+                next_state->whichClauses[-2*toInt(lit_)-1].erase(one_it);
             }
+
         }
-            next_state->clauses[cl_index].resize(0);
+        next_state->clauses[cl_index].resize(0);
     }
    
-    for(int j=0; j<inClauses_opposite.size(); j++)
+    for(map_int_int::iterator iter= inClauses_opposite.begin(); iter!=inClauses_opposite.end(); iter++)
     {
-        int cl_index_ = inClauses_opposite[j];
+        int cl_index_ = (*iter).first;
         par_Clause& cl_neg = next_state->clauses[cl_index_];
         cl_neg.remove(-toInt(lit));
             //becomes a unit clause
index 9ee99aea9cbd035de4c00d1066c4d13f6aa38cd9..ed4e5708d77044ea0ff13eaa68e45c50d11e4cd8 100644 (file)
@@ -1,6 +1,13 @@
 #ifndef _PAR_SOLVER_H
 #define _PAR_SOLVER_H
 
+#include <map>
+
+using namespace std;
+
+
+typedef map<int, int> map_int_int;
+
 class par_SolverState : public CMessage_par_SolverState {
 
 private:
@@ -34,7 +41,7 @@ public:
     CkVec<int>      occurrence; 
     CkVec<int>      positive_occurrence; 
     //2 * N (positive, negative)
-    CkVec< CkVec< int > >   whichClauses;
+    CkVec< map_int_int >   whichClauses;
     int             level;
    
     int             lower;
@@ -73,12 +80,10 @@ public:
        new_state->whichClauses.resize(_size); 
        for(int i=0; i<_size; i++)
        {
-           int _sub_size = org->whichClauses[i].size();
-           new_state->whichClauses[i].resize(_sub_size);
-
-           for(int j=0; j<_sub_size; j++)
+           map<int, int> __cl_copy = org->whichClauses[i];
+           for(map_int_int::iterator iter=__cl_copy.begin(); iter!=__cl_copy.end(); iter++)
            {
-               new_state->whichClauses[i][j] = org->whichClauses[i][j];
+               (new_state->whichClauses[i]).insert( pair<int, int>((*iter).first, (*iter).second));
            }
        }
        return new_state;