satisfiability can be run as sequential in order to get speed up
authorYanhua YanhuaSunLaptop <yanhuasun@vpn3-14483.near.uiuc.edu>
Fri, 2 Apr 2010 17:53:15 +0000 (12:53 -0500)
committerYanhua YanhuaSunLaptop <yanhuasun@vpn3-14483.near.uiuc.edu>
Fri, 2 Apr 2010 17:53:15 +0000 (12:53 -0500)
examples/charm++/satisfiability/Makefile
examples/charm++/satisfiability/main.C
examples/charm++/satisfiability/par_Solver.C
examples/charm++/satisfiability/par_Solver.h

index 5e66b56b2536427f3d3a42fbc8e8ef4d4c36cdd3..7bd90206dd12599f3782a7d3b55dd34ad5fb0ab8 100644 (file)
@@ -21,7 +21,7 @@ parsat_minisat: $(MINISAT)/Solver.o par_Solver_minisat.o main.o
 
 
 main.o : main.C main.decl.h main.def.h 
-       $(CXX_COMPILE) -o main.o -c main.C
+       $(CXX_COMPILE) $(CMINISATFLAGS) -o main.o -c main.C
 
 par_Solver_minisat.o : par_Solver.C par_SolverTypes.h par_Solver.h $(MINISAT)/SolverTypes.h  main.decl.h main.def.h 
        $(CXX_COMPILE) $(CMINISATFLAGS) -o par_Solver_minisat.o -c par_Solver.C
index 868843edb1b5620e8773b70e6ec0502285e7a546..86a49103896c8a1bf79d9f2a2ce8de369c64d3fa 100644 (file)
@@ -7,12 +7,23 @@
 #include <signal.h>
 #include <zlib.h>
 
+#include <vector>
+
 #include "main.decl.h"
 #include "main.h"
 
 #include "par_SolverTypes.h"
 #include "par_Solver.h"
 
+#ifdef MINISAT
+#include "Solver.h"
+#endif
+
+#ifdef TNM
+#include "TNM.h"
+#endif
+
+using namespace std;
 
 //#include "util.h"
 
@@ -99,7 +110,6 @@ static void readClause(StreamBuffer& in, par_SolverState& S, CkVec<par_Lit>& lit
         S.occurrence[var]++;
         if(parsed_lit>0)
             S.positive_occurrence[var]++;
-        //while (var >= S.nVars()) S.newVar();
         lits.push_back( par_Lit(parsed_lit));
     }
 }
@@ -118,7 +128,6 @@ static void simplify(par_SolverState& S)
         //only one element in unit clause
         par_Lit lit = cl[0];
         S.clauses[S.unit_clause_index[i]].resize(0);
-        S.unsolved_clauses--;
 
         int pp_ = 1;
         int pp_i_ = 2;
@@ -134,10 +143,6 @@ static void simplify(par_SolverState& S)
        CkVec<int> &inClauses = S.whichClauses[pp_*2*toInt(lit)-pp_i_];
        CkVec<int> &inClauses_opposite = S.whichClauses[pp_*2*toInt(lit)-pp_j_];
        
-#ifdef DEBUG
-        CkPrintf("****\nUnit clause is %d, index=%d, occurrence=%d\n", toInt(lit), S.unit_clause_index[i], -pp_i_);
-           CkPrintf("\t same occur");
-#endif
        // literal with same sign
        for(int j=0; j<inClauses.size(); j++)
        {
@@ -161,7 +166,8 @@ static void simplify(par_SolverState& S)
                    S.positive_occurrence[toInt(lit_)-1]--;
                    //S.whichClauses[2*toInt(lit_)-2].remove(cl_index);
                 //remove the clause index for the literal
-               for(int _i = 0; _i<S.whichClauses[2*toInt(lit_)-2].size(); _i++)
+                    /* 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)
                        {
@@ -183,7 +189,6 @@ static void simplify(par_SolverState& S)
                }
            }
            
-           S.unsolved_clauses--;
            S.clauses[cl_index].resize(0); //this clause goes away. In order to keep index unchanged, resize it as 0
        }
        
@@ -225,7 +230,6 @@ static void parse_confFile(gzFile input_stream, par_SolverState& S) {
                 
 
                 S.var_size = vars;
-                S.unsolved_vars = vars;
                 S.occurrence.resize(vars);
                 S.positive_occurrence.resize(vars);
                 S.whichClauses.resize(2*vars);
@@ -268,8 +272,6 @@ Main::Main(CkArgMsg* msg)
 
     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 */
 
     starttimer = CmiWallTimer();
@@ -286,10 +288,8 @@ Main::Main(CkArgMsg* msg)
 
     parse_confFile(in, *solver_msg);
 
-
     /*  unit propagation */ 
     simplify(*solver_msg);
-
 #ifdef DEBUG
     for(int __i = 0; __i<solver_msg->occurrence.size(); __i++)
     {
@@ -297,31 +297,57 @@ Main::Main(CkArgMsg* msg)
         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]);
         }
     }
 
-
-    CkPrintf(" unsolved clauses %d\n", solver_msg->unsolvedClauses());
 #endif
 
-    solver_msg->unsolved_clauses = 0;
-   
     int unsolved = solver_msg->unsolvedClauses();
 
     if(unsolved == 0)
     {
         CkPrintf(" This problem is solved by pre-processing\n");
-        //solver_msg->printSolution();
         CkExit();
     }
     readfiletimer = CmiWallTimer();
     /*fire the first chare */
     /* 1)Which variable is assigned which value this time, (variable, 1), current clauses status vector(), literal array activities */
 
+
+    /***  If grain size is larger than the clauses size, that means 'sequential' */
+    if(grainsize > solver_msg->clauses.size())
+    {
+        vector< vector<int> > seq_clauses;
+        for(int _i_=0; _i_<solver_msg->clauses.size(); _i_++)
+        {
+            if(solver_msg->clauses[_i_].size() > 0)
+            {
+                vector<int> unsolvedclaus;
+                par_Clause& cl = solver_msg->clauses[_i_];
+                unsolvedclaus.resize(cl.size());
+                for(int _j_=0; _j_<cl.size(); _j_++)
+                {
+                    unsolvedclaus[_j_] = toInt(cl[_j_]);
+                }
+                seq_clauses.push_back(unsolvedclaus);
+            }
+        }
+        bool satisfiable_1 = seq_processing(solver_msg->var_size, seq_clauses);//seq_solve(next_state);
+
+        if(satisfiable_1)
+        {
+            CkPrintf("One solution found without using any parallel\n");
+        }else
+        {
+       
+            CkPrintf(" Unsatisfiable\n");
+        }
+        done(solver_msg->occurrence);
+        return;
+    }
     mainProxy = thisProxy;
     int max_index = get_max_element(solver_msg->occurrence);
     
@@ -329,7 +355,6 @@ Main::Main(CkArgMsg* msg)
     solver_msg->level = 0;
     par_SolverState *not_msg = copy_solverstate(solver_msg);
     
-    //CkPrintf(" main chare max index=%d, %d, assigned=%d\n", max_index+1, solver_msg->occurrence[max_index], toInt(solver_msg->assigned_lit));
     solver_msg->occurrence[max_index] = -2;
     not_msg->assigned_lit = par_Lit(-max_index-1);
     not_msg->occurrence[max_index] = -1;
@@ -376,7 +401,8 @@ 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);
@@ -386,7 +412,7 @@ void Main::done(CkVec<int> assignment)
     {
         fprintf(file, "%d\n", assignment[i]);
     }
-    
+    */
     CkExit();
 }
 #include "main.def.h"
index 8d9ee4586f9bd94f0367e9181743658b7a948811..22a472f6b72bddcd69e51b209e232f6e07d0c4f3 100644 (file)
@@ -19,25 +19,14 @@ extern int grainsize;
 
 par_SolverState::par_SolverState()
 {
-    unsolved_clauses = 0; 
     var_frequency = 0;
 }
 
-inline int par_SolverState::nVars()
-{
-    return var_frequency; 
-}
 
 int par_SolverState::clausesSize()
 {
     return clauses.size();
 }
-int par_SolverState::newVar(bool sign, bool dvar)
-{
-    int v = nVars();
-    var_frequency++;
-    return v;
-}
 
 void par_SolverState::attachClause(par_Clause& c)
 {
@@ -84,10 +73,6 @@ bool par_SolverState::addClause(CkVec<par_Lit>& ps)
                 CkPrintf("clause conflict between %d and %d\n", index, clauses.size());
                 return false;
             }
-            /*else if(unit_lit == ps[0])
-            {
-                return true;
-            }*/
         }
        /* all unit clauses are checked, no repeat, no conflict */
         unit_clause_index.push_back(clauses.size());
@@ -117,7 +102,6 @@ bool par_SolverState::addClause(CkVec<par_Lit>& ps)
     }
     clauses.push_back(par_Clause());
     clauses[clauses.size()-1].attachdata(ps, false);
-    unsolved_clauses++;
     // build the linklist for each literal pointing to the clause, where the literal occurs
     for(int i=0; i< ps.size(); i++)
     {
@@ -153,7 +137,6 @@ mySolver::mySolver(par_SolverState* state_msg)
     CkPrintf("\n\nNew chare: literal = %d, occurrence size=%d, level=%d \n", toInt(lit), state_msg->occurrence.size(), state_msg->level);
 #endif    
     par_SolverState *next_state = copy_solverstate(state_msg);
-    //next_state->unsolved_vars = state_msg->unsolved_vars - 1;
 
     //Unit clauses
     /* use this value to propagate the clauses */
@@ -251,7 +234,6 @@ mySolver::mySolver(par_SolverState* state_msg)
        lit = cl[0];
 
 
-       //next_state->unsolved_vars--;
     }
     /***************/
 
@@ -319,7 +301,7 @@ mySolver::mySolver(par_SolverState* state_msg)
                 seq_clauses.push_back(unsolvedclaus);
             }
         }
-        satisfiable_1 = seq_processing(next_state->unsolved_vars, seq_clauses);//seq_solve(next_state);
+        satisfiable_1 = seq_processing(next_state->var_size, seq_clauses);//seq_solve(next_state);
         if(satisfiable_1)
         {
             CkPrintf("One solution found by sequential processing \n");
@@ -367,7 +349,7 @@ mySolver::mySolver(par_SolverState* state_msg)
             }
         }
 
-        bool ret = seq_processing(new_msg2->unsolved_vars,  seq_clauses);//seq_solve(next_state);
+        bool ret = seq_processing(new_msg2->var_size,  seq_clauses);//seq_solve(next_state);
         //bool ret = Solver::seq_processing(new_msg2->clauses);//seq_solve(new_msg2);
         if(ret)
         {
index b6d4fbabaa5f17fb36ba8f060da3036f1e3f555e..9ee99aea9cbd035de4c00d1066c4d13f6aa38cd9 100644 (file)
@@ -10,11 +10,8 @@ public:
     
     par_SolverState();
 
-    int nVars();
-
     int clausesSize();
     
-    int newVar (bool polarity = true, bool dvar = true);
     
     bool addClause(CkVec<par_Lit>& lits);
 
@@ -29,7 +26,6 @@ public:
     CkVec<par_Clause>   clauses;
     par_Lit             assigned_lit;
     int             var_size;
-    int             unsolved_vars;
     int             unsolved_clauses;
 
     int             var_frequency; // 1, -1, 1 freq = 3
@@ -66,7 +62,6 @@ public:
        }
 
        new_state->var_size = org->var_size;
-       new_state->unsolved_vars = org->unsolved_vars;
        new_state->occurrence.resize(org->occurrence.size());
        new_state->positive_occurrence.resize(org->occurrence.size());
        for(int _i=0; _i<org->occurrence.size(); _i++){