fix a bug that occur in sequential part in satisfiability problem
authorYanhua YanhuaSunLaptop <yanhuasun@yanhua-suns-macbook-pro.local>
Wed, 24 Mar 2010 05:00:48 +0000 (00:00 -0500)
committerYanhua YanhuaSunLaptop <yanhuasun@yanhua-suns-macbook-pro.local>
Wed, 24 Mar 2010 05:00:48 +0000 (00:00 -0500)
examples/charm++/satisfiability/Solver.C
examples/charm++/satisfiability/main.C
examples/charm++/satisfiability/verify/Makefile
examples/charm++/satisfiability/verify/verify.C

index e1f86ac41fc1cfe70bae250cce1abc55da0501cf..7e0f09423e703217ade764955ac43b7ec2f0a58b 100644 (file)
@@ -36,7 +36,6 @@ void SolverState::attachClause(Clause& c)
 
 }
 
-
 int SolverState::unsolvedClauses()
 {
     int unsolved = 0;
@@ -53,12 +52,7 @@ void SolverState::printSolution()
 {
     for(int _i=0; _i<var_size; _i++)
     {
-        if(occurrence[_i] == -2)
-            CkPrintf(" TRUE ");
-        else if(occurrence[_i] == -1)
-            CkPrintf(" FALSE ");
-        else
-            CkPrintf(" Anything ");
+        CkPrintf("%d\n", occurrence[_i]);
     }
  
 }
@@ -156,100 +150,96 @@ Solver::Solver(SolverState* state_msg)
     /* use this value to propagate the clauses */
     // deal with the clauses where this literal is
     int _unit_ = -1;
-   
-unit_propagation:while(1){
-    int pp_ = 1;
-    int pp_i_ = 2;
-    int pp_j_ = 1;
-
-    if(toInt(lit) < 0)
-    {
-        pp_ = -1;
-        pp_i_ = 1;
-        pp_j_ = 2;
-    }
-
-    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_];
-
-    // literal with same sign, remove all these clauses
-    for(int j=0; j<inClauses.size(); j++)
-    {
-        int cl_index = inClauses[j];
+    while(1){
+        int pp_ = 1;
+        int pp_i_ = 2;
+        int pp_j_ = 1;
 
-        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++)
+        if(toInt(lit) < 0)
         {
-            Lit lit_ = cl_[k];
-            if(toInt(lit_) == toInt(lit))
-                continue;
-            next_state->occurrence[abs(toInt(lit_)) - 1]--;
-            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;
-                    }
-                }
-            }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;
-                    }
-                }
-            }
+            pp_ = -1;
+            pp_i_ = 1;
+            pp_j_ = 2;
         }
-            next_state->clauses[cl_index].resize(0);
 
-    }
-   
-    for(int j=0; j<inClauses_opposite.size(); j++)
-    {
-        int cl_index_ = inClauses_opposite[j];
-        Clause& cl_neg = next_state->clauses[cl_index_];
-        cl_neg.remove(-toInt(lit));
-        
-        //becomes a unit clause
-         if(cl_neg.size() == 1)
-         {
-             next_state->unit_clause_index.push_back(cl_index_);
-         }else if (cl_neg.size() == 0)
-         {
-                return;
-         }
-    }
+        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_];
 
-    _unit_++;
-    if(_unit_ == next_state->unit_clause_index.size())
-        break;
-    Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
-
-    while(cl.size() == 0){
-        _unit_++;
-        if(_unit_ == next_state->unit_clause_index.size())
-            break;
-        cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
-        
-    };
-
-    if(_unit_ == next_state->unit_clause_index.size())
-        break;
-    lit = cl[0];
+    // literal with same sign, remove all these clauses
+       for(int j=0; j<inClauses.size(); j++)
+       {
+           int cl_index = inClauses[j];
+
+           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++)
+           {
+               Lit lit_ = cl_[k];
+               if(toInt(lit_) == toInt(lit))
+                   continue;
+               next_state->occurrence[abs(toInt(lit_)) - 1]--;
+               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;
+                       }
+                   }
+               }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;
+                       }
+                   }
+               }
+           } //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++)
+       {
+           int cl_index_ = inClauses_opposite[j];
+           Clause& cl_neg = next_state->clauses[cl_index_];
+           cl_neg.remove(-toInt(lit));
+
+           /*becomes a unit clause */
+           if(cl_neg.size() == 1)
+           {
+               next_state->unit_clause_index.push_back(cl_index_);
+           }else if (cl_neg.size() == 0)
+           {
+               return;
+           }
+       }
+
+       _unit_++;
+       if(_unit_ == next_state->unit_clause_index.size())
+           break;
+       Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+
+       while(cl.size() == 0){
+           _unit_++;
+           if(_unit_ == next_state->unit_clause_index.size())
+               break;
+           cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+       };
+
+       if(_unit_ == next_state->unit_clause_index.size())
+           break;
+       lit = cl[0];
     }
     /***************/
 
@@ -257,11 +247,7 @@ unit_propagation:while(1){
     if(unsolved == 0)
     {
         CkPrintf("One solution found in parallel processing \n");
-        
-#ifdef SOLUTION
-        next_state->printSolution();
-#endif
-
+        //next_state->printSolution();
         mainProxy.done(next_state->occurrence);
         return;
     }
@@ -274,7 +260,6 @@ unit_propagation:while(1){
    
     /* the other branch */
     SolverState *new_msg2 = copy_solverstate(next_state);;
-    new_msg2->var_size = state_msg->var_size;
 
     next_state->level = state_msg->level+1;
 
@@ -293,7 +278,6 @@ unit_propagation:while(1){
         next_state->occurrence[max_index] = -1;
     }
     bool satisfiable_1 = true;
-    bool satisfiable_0 = true;
 
     if(unsolved > grainsize)
     {
@@ -308,8 +292,6 @@ unit_propagation:while(1){
         satisfiable_1 = seq_solve(next_state);
         if(satisfiable_1)
         {
-            CkPrintf(" One solutions found by sequential algorithm\n");
-            mainProxy.done(next_state->occurrence);
             return;
         }
     }
@@ -328,7 +310,6 @@ unit_propagation:while(1){
     unsolved = new_msg2->unsolvedClauses();
     if(unsolved > grainsize)
     {
-
         new_msg2->lower = middle + 1;
         new_msg2->higher = higher-1;
         *((int *)CkPriorityPtr(new_msg2)) = middle+1;
@@ -337,15 +318,7 @@ unit_propagation:while(1){
     }
     else
     {
-        satisfiable_0 = seq_solve(new_msg2);
-
-        if(satisfiable_0)
-        {
-            CkPrintf(" One solutions found by sequential algorithm\n");
-            mainProxy.done(new_msg2->occurrence);
-            return;
-        }
-
+        seq_solve(new_msg2);
     }
 
 }
@@ -441,7 +414,6 @@ bool Solver::seq_solve(SolverState* state_msg)
              next_state->unit_clause_index.push_back(cl_index_);
          }else if (cl_neg.size() == 0)
          {
-    //            CkPrintf(" conflict found in seqential testing!\n");
                 return false;
          }
     }
@@ -465,14 +437,11 @@ bool Solver::seq_solve(SolverState* state_msg)
     lit = cl[0];
     }
    
-   
     int unsolved = next_state->unsolvedClauses();
     if(unsolved == 0)
     {
-        CkPrintf("One solution found\n");
-#ifdef SOLUTION
-        next_state->printSolution();
-#endif
+        CkPrintf("One solution found in sequential processing, check the output file for assignment\n");
+        mainProxy.done(next_state->occurrence);
         return true;
     }
     
@@ -487,9 +456,10 @@ bool Solver::seq_solve(SolverState* state_msg)
 #ifdef DEBUG
         CkPrintf("max index = %d\n", max_index);
 #endif
-        next_state->var_size = state_msg->var_size;
         next_state->level = state_msg->level+1;
 
+        SolverState *new_msg2 = copy_solverstate(next_state);;
+        
         int positive_max = next_state->positive_occurrence[max_index];
         if(positive_max >= next_state->occurrence[max_index] - positive_max)
         {
@@ -508,19 +478,20 @@ bool Solver::seq_solve(SolverState* state_msg)
             return true;
         }
         
+        new_msg2->level = state_msg->level+1;
        
         if(positive_max >= next_state->occurrence[max_index] - positive_max)
         {
-            next_state->occurrence[max_index] = -1;
-            next_state->assigned_lit = Lit(-max_index-1);
+            new_msg2->occurrence[max_index] = -1;
+            new_msg2->assigned_lit = Lit(-max_index-1);
         }
         else
         {
-            next_state->occurrence[max_index] = -2;
-            next_state->assigned_lit = Lit(max_index+1);
+            new_msg2->occurrence[max_index] = -2;
+            new_msg2->assigned_lit = Lit(max_index+1);
         } 
             
-        bool satisfiable_0 = seq_solve(next_state);
+        bool satisfiable_0 = seq_solve(new_msg2);
         if(satisfiable_0)
         {
             return true;
index 7368d0a065e8d8ac442b93dc0f1506de688aca7f..715404866c0ba4bae4ebc704cd5b18c201128850 100644 (file)
@@ -263,6 +263,9 @@ Main::Main(CkArgMsg* msg)
     }else
         grainsize = atoi(msg->argv[2]);
 
+
+    CkPrintf("problem file:\t\t%s\ngrainsize:\t\t%d\nprocessor number:\t\t%d\n", msg->argv[1], grainsize, CkNumPes()); 
+
     char filename[50];
 
     /* read file */
@@ -288,13 +291,15 @@ Main::Main(CkArgMsg* msg)
 #ifdef DEBUG
     for(int __i = 0; __i<solver_msg->occurrence.size(); __i++)
     {
-
-            if(solver_msg->occurrence[__i] == -2)
-                CkPrintf(" TRUE ");
-            else if(solver_msg->occurrence[__i] == -1)
-                CkPrintf(" FALSE ");
-            else
-                CkPrintf(" UNDECIDED ");
+        FILE *file;
+        char outputfile[50];
+        sprintf(outputfile, "%s.sat", inputfile);
+        file = fopen(outputfile, "w");
+
+        for(int i=0; i<assignment.size(); i++)
+        {
+            fprintf(file, "%d\n", assignment[i]);
+        }
     }
 
 
@@ -308,7 +313,7 @@ Main::Main(CkArgMsg* msg)
     if(unsolved == 0)
     {
         CkPrintf(" This problem is solved by pre-processing\n");
-        solver_msg->printSolution();
+        //solver_msg->printSolution();
         CkExit();
     }
     readfiletimer = CmiWallTimer();
@@ -371,17 +376,13 @@ void Main::done(CkVec<int> assignment)
     CkPrintf("Solving time:                             %f\n", endtimer - readfiletimer);
   
     FILE *file;
-
     char outputfile[50];
     sprintf(outputfile, "%s.sat", inputfile);
-    file = fopen(outputfile, "a+");
+    file = fopen(outputfile, "w");
 
     for(int i=0; i<assignment.size(); i++)
     {
-        if(assignment[i] == -1)
-            fprintf(file, "%d\n", -1);
-        else
-            fprintf(file, "%d\n", 1);
+        fprintf(file, "%d\n", assignment[i]);
     }
     
     CkExit();
index 50d8a6e3a3da0ae0b3cf41aa205543be133ba6c6..39e73c06637d59adfb428168ee04c7b3d23a5b38 100644 (file)
@@ -1,10 +1,10 @@
 CXX = g++
 FLAGS = $(OPTS) 
 
-verify:verify.o
-       $(CXX) -lz -o verify verify.o
+runverify:verify.o
+       $(CXX) -lz -o runverify verify.o
 verify.o:verify.C
        $(CXX) $(FLAGS) -o verify.o -c verify.C
 
 clean:
-       rm *.o verify
+       rm *.o runverify
index 2b93806d4a0ecd5d840ff7a934773d209c0daa49..21f4c30d640d0433a9f48645d9ded59a55a2cedd 100644 (file)
@@ -136,14 +136,12 @@ static void parse_confFile( char* solution_file, gzFile problem_stream) {
             for (;;){
                 parsed_lit = parseInt(in);
 
-                if(parsed_lit>0 && assignment[parsed_lit-1]==1)
+                if(parsed_lit>0 && (assignment[parsed_lit-1]==-2 || assignment[parsed_lit-1]==0))
                 {
-                    //printf("%d=%d ", parsed_lit, assignment[parsed_lit-1]);
                     satisfied = true;
                 }
-                if(parsed_lit<0 && assignment[-parsed_lit-1]==-1)
+                if(parsed_lit<0 && (assignment[-parsed_lit-1]==-1 || assignment[-parsed_lit-1]==0))
                 {
-                    //printf("%d=%d ", parsed_lit, assignment[-parsed_lit-1]);
                     satisfied = true;
                 }