modify data structure in satisfiability example
authorYanhua YanhuaSunLaptop <yanhuasun@vpn3-14460.near.uiuc.edu>
Tue, 23 Mar 2010 15:43:11 +0000 (10:43 -0500)
committerYanhua YanhuaSunLaptop <yanhuasun@vpn3-14460.near.uiuc.edu>
Tue, 23 Mar 2010 15:43:11 +0000 (10:43 -0500)
examples/charm++/satisfiability/Makefile
examples/charm++/satisfiability/Solver.C
examples/charm++/satisfiability/Solver.h
examples/charm++/satisfiability/SolverTypes.h
examples/charm++/satisfiability/example_simple.cnf
examples/charm++/satisfiability/main.C

index ae22ab6761dcc08809c9dc96295b7c5c7814634d..ae849affef24d737c1bff09d27f47f09dbdc8de1 100644 (file)
@@ -10,7 +10,7 @@ sat : main.o Solver.o
 main.o : main.C main.decl.h main.def.h 
        $(CHARMC) -o main.o main.C 
 
-Solver.o : Solver.C SolverTypes.h
+Solver.o : Solver.C SolverTypes.h Solver.h
        $(CHARMC) -o Solver.o Solver.C
 
 #util.o : util.C
index 3cdc12023b81bc5873d732776e62815369e68323..fdd2af6d7dbcbf07999378ef0a7f95f29a0e04cc 100644 (file)
@@ -11,7 +11,7 @@ extern int grainsize;
 
 SolverState::SolverState()
 {
-
+    unsolved_clauses = 0; 
     var_frequency = 0;
 }
 
@@ -20,6 +20,10 @@ inline int SolverState::nVars()
     return var_frequency; 
 }
 
+int SolverState::clausesSize()
+{
+    return clauses.size();
+}
 Var SolverState::newVar(bool sign, bool dvar)
 {
     int v = nVars();
@@ -84,6 +88,19 @@ bool SolverState::addClause(CkVec<Lit>& ps)
     }
     clauses.push_back(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++)
+    {
+        Lit lit = ps[i];
+
+        if(toInt(lit) > 0)
+            whichClauses[2*toInt(lit)-2].push_back(clauses.size()-1);
+        else
+            whichClauses[-2*toInt(lit)-1].push_back(clauses.size()-1);
+
+    }
+
     return true;
 }
 
@@ -103,267 +120,184 @@ Solver::Solver(SolverState* state_msg)
 
     CkVec<Clause> next_clauses;
     /* Which variable get assigned  */
-    Lit assigned_var = state_msg->assigned_lit;
+    Lit lit = state_msg->assigned_lit;
 #ifdef DEBUG    
-    CkPrintf("\n\nNew chare: literal = %d, occurrence size=%d, level=%d \n", toInt(assigned_var), state_msg->occurrence.size(), state_msg->level);
+    CkPrintf("\n\nNew chare: literal = %d, occurrence size=%d, level=%d \n", toInt(lit), state_msg->occurrence.size(), state_msg->level);
 #endif    
     SolverState *next_state = copy_solverstate(state_msg);
     
     //Unit clauses
-    map<int, int>  unit_clauses;
-
     /* use this value to propagate the clauses */
-    for(int i=0; i<(state_msg->clauses).size(); i++)
+    // deal with the clauses where this literal is
+    int _unit_ = -1;
+    while(1){
+    int pp_ = 1;
+    int pp_i_ = 2;
+    int pp_j_ = 1;
+
+    if(toInt(lit) < 0)
     {
-        Clause cl = ((state_msg->clauses)[i]);
-        CkVec<Lit> new_clause;
-        bool satisfied = false;
-#ifdef DEBUG    
-//        CkPrintf("\n");
-#endif
-        for(int j=0; j<cl.size();  j++)
-        {
-            Lit lit = cl[j];
-#ifdef DEBUG    
-        //    CkPrintf("%d   ", toInt(lit));
-#endif
-            if(lit == assigned_var)
-            {
-                satisfied = true;
-                break;
-            }else if( lit == ~(assigned_var))
-            {
-            } else
-            {
-                new_clause.push_back(lit);
-            }
-        }
-        if(satisfied)
+        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];
+
+        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++)
         {
-            for(int j=0; j<cl.size();  j++)
+            Lit lit_ = cl_[k];
+            if(toInt(lit_) == toInt(lit))
+                continue;
+            next_state->occurrence[abs(toInt(lit_)) - 1]--;
+            if(toInt(lit_) > 0)
             {
-                Lit lit = cl[j];
-                if(lit != assigned_var)
+                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++)
                 {
-                    int int_lit = toInt(lit);
-                    (next_state->occurrence[abs(int_lit)-1])--;
-                    if(int_lit > 0)
-                        (next_state->positive_occurrence[abs(int_lit)-1])--;
+                    if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
+                    {
+                        next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
+                        break;
+                    }
                 }
-            }
-        } else if(new_clause.size() == 0 )
-        {
-        
-            /* conflict */
-            return;
-        }else if(new_clause.size() == 1)
-        {
-            /*unit clause */
-            Lit lit = new_clause[0];
-            if(unit_clauses.find(-toInt(lit)) !=unit_clauses.end())
-            {
-#ifdef DEBUG
-                CkPrintf("conflict detected by unit progation, size=%d\n", unit_clauses.size());
-#endif
-                return;
-                /* conflict*/
             }else
             {
-                (unit_clauses[toInt(lit)])++;
-                int int_lit = toInt(lit);
-                int_lit>0?state_msg->occurrence[int_lit-1]=-2:state_msg->occurrence[-int_lit-1]=-1;
-#ifdef DEBUG
-                CkPrintf(" unit clause %d=%d, size=%D\n", toInt(lit), unit_clauses[toInt(lit)], unit_clauses.size());
-#endif
-            }
-        }
-        else if(new_clause.size() > 1)
-        {
-            Clause clsc(new_clause, false);
-            next_clauses.push_back(clsc);
-        }
-    } /* all clauses are checked*/
-   
-    if(next_clauses.size() == 0)
-    {
-        /* one solution is found*/
-        /* print the solution*/
-        CkPrintf("one solutions found level=%d parallel\n", state_msg->level);
-       /* 
-        for(int _i=0; _i<state_msg->var_size; _i++)
-        {
-            if(state_msg->occurrence[_i] == -2)
-                CkPrintf(" TRUE ");
-            else if(state_msg->occurrence[_i] == -1)
-                CkPrintf(" FALSE ");
-            else
-                CkPrintf(" Anything ");
-        }*/
-        CkPrintf("\n");
-        mainProxy.done();//highest priority
-        //CkExit();
-        return;
-    }else
-    {
-        /* make a decision and then fire new tasks */
-        /* if there is unit clause, should choose these first??? TODO */
-        /* TODO which variable to pick up */
-        /*unit clause literal and also which occurrs most times */
-        while(!unit_clauses.empty())
-        {
-           //CkPrintf(" parallel propagation unit clauses size=%d, non unit size=%d, assigned var=%d\n", unit_clauses.size(), next_clauses.size(), toInt(assigned_var));
-            int first_unit = (*(unit_clauses.begin())).first;
-           //assign this variable
-            for(int _i=0; _i<next_clauses.size(); _i++)
-            {
-                Clause& cl = next_clauses[_i];
-               
-                //reduce the clause
-                for(int j=0; j<cl.size(); j++)
+                for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
                 {
-                    Lit lit = cl[j];
-                    if(toInt(lit) == first_unit)//this clause goes away
-                    {
-                        for(int jj=0; jj<cl.size(); jj++)
-                        {
-                            Lit lit_2 = cl[jj];
-                            (next_state->occurrence[abs(toInt(lit_2))-1])--; 
-                            if(toInt(lit_2) > 0)
-                                (next_state->positive_occurrence[abs(toInt(lit_2))-1])--; 
-                        }
-                        next_clauses.remove(_i);
-                        _i--;
-                       break; 
-                    }else if (toInt(lit) == -first_unit)
+                    if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
                     {
-                        cl.remove(j);
-                        j--;
+                        next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
+                        break;
                     }
                 }
-                if(cl.size()==0){ // conflict
-                    return;
-                }else if(cl.size() == 1)// new unit clause
-                {
-                    unit_clauses[toInt(cl[0])]++;
-                
-                    next_clauses.remove(_i);
-                    _i--;
-                }
             }
-            /*remove this unit clause */
-            unit_clauses.erase(unit_clauses.begin());
-        }
-
         }
-
-    if(next_clauses.size() == 0)
+            next_state->clauses[cl_index].resize(0);
+    }
+   
+    for(int j=0; j<inClauses_opposite.size(); j++)
     {
-        CkPrintf(" one solutions found after propagation \n");
-        mainProxy.done();
-        //CkExit();
-        return;
+        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)
+         {
+                CkPrintf(" conflict found!\n");
+                return;
+         }
+    }
+    _unit_++;
+    if(_unit_ == next_state->unit_clause_index.size())
+        break;
+    Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
+    lit = cl[0];
     }
-        int max_index = get_max_element(next_state->occurrence);
+    /***************/    
+    int max_index = get_max_element(next_state->occurrence);
 #ifdef DEBUG
-        CkPrintf("max index = %d\n", max_index);
+    CkPrintf("max index = %d\n", max_index);
 #endif
-        if(next_state->occurrence[max_index] <=0)
-        {
-            CkPrintf("Unsatisfiable\n");
-            mainProxy.done();
-            //CkExit();
-            return;
-        }
-
-
-        //if() left literal unassigned is larger than a grain size, parallel 
-        /* When we start sequential 3SAT Grainsize problem*/
-        next_state->assignclause(next_clauses);
-        next_state->var_size = state_msg->var_size;
-
-        SolverState *new_msg2 = copy_solverstate(next_state);;
-        new_msg2->var_size = state_msg->var_size;
+    if(max_index < 0)
+    {
+        CkPrintf("One solution found\n");
+        mainProxy.done();
+        return;
+    }
+    //if() left literal unassigned is larger than a grain size, parallel 
+    ///* When we start sequential 3SAT Grainsize problem*/
+    
+    SolverState *new_msg2 = copy_solverstate(next_state);;
+    new_msg2->var_size = state_msg->var_size;
 
-        next_state->level = state_msg->level+1;
-       
+    next_state->level = state_msg->level+1;
 
-        int lower = state_msg->lower;
-        int higher = state_msg->higher;
-        int middle = (lower+higher)/2;
-        int positive_max = next_state->positive_occurrence[max_index];
-        if(positive_max >= next_state->occurrence[max_index] - positive_max)
-        {
-            next_state->assigned_lit = Lit(max_index+1);
-            next_state->occurrence[max_index] = -2;
-        }
-        else
-        {
-            next_state->assigned_lit = Lit(-max_index-1);
-            next_state->occurrence[max_index] = -1;
-        }
-        bool satisfiable_1 = true;
-        bool satisfiable_0 = true;
-
-        if(next_state->clauses.size() > grainsize)
-        {
-            next_state->lower = lower + 1;
-            next_state->higher = middle;
-            *((int *)CkPriorityPtr(next_state)) = lower+1;
-            CkSetQueueing(next_state, CK_QUEUEING_IFIFO);
-            CProxy_Solver::ckNew(next_state);
-        }
-        else //sequential
-        {
-            satisfiable_1 = seq_solve(next_state);
-            if(satisfiable_1)
-            {
-                CkPrintf(" One solutions found by sequential algorithm\n");
-                mainProxy.done();
-                //CkExit();
-                return;
-            }
-        }
+    int lower = state_msg->lower;
+    int higher = state_msg->higher;
+    int middle = (lower+higher)/2;
+    int positive_max = next_state->positive_occurrence[max_index];
+    if(positive_max >= next_state->occurrence[max_index] - positive_max)
+    {
+        next_state->assigned_lit = Lit(max_index+1);
+        next_state->occurrence[max_index] = -2;
+    }
+    else
+    {
+        next_state->assigned_lit = Lit(-max_index-1);
+        next_state->occurrence[max_index] = -1;
+    }
+    bool satisfiable_1 = true;
+    bool satisfiable_0 = true;
 
-        new_msg2->level = state_msg->level+1;
-        if(positive_max >= new_msg2->occurrence[max_index] - positive_max)
-        {
-            new_msg2->assigned_lit = Lit(-max_index-1);
-            new_msg2->occurrence[max_index] = -1;
-        }
-        else
-        {
-            new_msg2->assigned_lit = Lit(max_index+1);
-            new_msg2->occurrence[max_index] = -2;
-        }
-        if(new_msg2->clauses.size() > grainsize)
+    if(next_state->clauses.size() > grainsize)
+    {
+        next_state->lower = lower + 1;
+        next_state->higher = middle;
+        *((int *)CkPriorityPtr(next_state)) = lower+1;
+        CkSetQueueing(next_state, CK_QUEUEING_IFIFO);
+        CProxy_Solver::ckNew(next_state);
+    }
+    else //sequential
+    {
+        satisfiable_1 = seq_solve(next_state);
+        if(satisfiable_1)
         {
-
-            new_msg2->lower = middle + 1;
-            new_msg2->higher = higher-1;
-            *((int *)CkPriorityPtr(new_msg2)) = middle+1;
-            CkSetQueueing(new_msg2, CK_QUEUEING_IFIFO);
-            CProxy_Solver::ckNew(new_msg2);
+            CkPrintf(" One solutions found by sequential algorithm\n");
+            mainProxy.done();
+            return;
         }
-        else
-        {
-            satisfiable_0 = seq_solve(new_msg2);
+    }
 
-            if(satisfiable_0)
-            {
-                CkPrintf(" One solutions found by sequential algorithm\n");
-                mainProxy.done();
-                //CkExit();
-                return;
-            }
+    new_msg2->level = state_msg->level+1;
+    if(positive_max >= new_msg2->occurrence[max_index] - positive_max)
+    {
+        new_msg2->assigned_lit = Lit(-max_index-1);
+        new_msg2->occurrence[max_index] = -1;
+    }
+    else
+    {
+        new_msg2->assigned_lit = Lit(max_index+1);
+        new_msg2->occurrence[max_index] = -2;
+    }
+    if(new_msg2->clauses.size() > grainsize)
+    {
 
-        }
+        new_msg2->lower = middle + 1;
+        new_msg2->higher = higher-1;
+        *((int *)CkPriorityPtr(new_msg2)) = middle+1;
+        CkSetQueueing(new_msg2, CK_QUEUEING_IFIFO);
+        CProxy_Solver::ckNew(new_msg2);
+    }
+    else
+    {
+        satisfiable_0 = seq_solve(new_msg2);
 
-        if(!satisfiable_1 && !satisfiable_0)
+        if(satisfiable_0)
         {
-            CkPrintf("Unsatisfiable through sequential\n");
+            CkPrintf(" One solutions found by sequential algorithm\n");
             mainProxy.done();
-            //CkExit();
+            return;
         }
+
+    }
+
 }
 
 /* Which literals are already assigned, which is assigned this interation, the unsolved clauses */
index 4699bcc0d1cd9c2b23b67bafa39eb965a6573f63..dd30738795de143bee2053b4574fda85a60acd60 100644 (file)
@@ -12,6 +12,8 @@ public:
 
     int nVars();
 
+    int clausesSize();
+    
     Var newVar (bool polarity = true, bool dvar = true);
     
     bool addClause(CkVec<Lit>& lits);
@@ -24,12 +26,15 @@ public:
     CkVec<Clause>   clauses;
     Lit             assigned_lit;
     int             var_size;
+    int             unsolved_clauses;
 
     int             var_frequency; // 1, -1, 1 freq = 3
     CkVec<int>      unit_clause_index;
     // -2 means true, -1 means false, 0 means anything, > 0 means occurrence
     CkVec<int>      occurrence; 
     CkVec<int>      positive_occurrence; 
+    //2 * N (positive, negative)
+    CkVec< CkVec< int > >   whichClauses;
     int             level;
    
     int             lower;
@@ -64,7 +69,19 @@ public:
            new_state->occurrence[_i] = org->occurrence[_i];
            new_state->positive_occurrence[_i] = org->occurrence[_i];
        }
-        new_state->level = org->level;
+       new_state->level = org->level;
+       int _size = org->whichClauses.size();
+       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++)
+           {
+               new_state->whichClauses[i][j] = org->whichClauses[i][j];
+           }
+       }
        return new_state;
     }
 
index 1a30e812841e31e9ba34e54c0968a4d64c96588c..e11ed2911c25e8337af84bd9f2ea3de4afe9ebcb 100644 (file)
@@ -28,9 +28,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 template<class V> 
 int get_max_element(const V& ps) {
 
-    int max_index = 0;
-    int max = ps[0];
-    for(int __i=1; __i<ps.size(); __i++)
+    int max_index = -1;
+    int max = -1;
+    for(int __i=0; __i<ps.size(); __i++)
     {
         if(ps[__i] > max)
         {
@@ -38,7 +38,6 @@ int get_max_element(const V& ps) {
             max_index = __i;
         }
     }
-
     return max_index;
 }
 
@@ -155,8 +154,15 @@ public:
         for (int i = 0; i < ps.size(); i++) data[i] = ps[i];
     }
 
-    void remove(int i){
-        data.remove(i); 
+    void remove(int v){
+        for(int i=0; i<data.size(); i++)
+        {
+            if(toInt(data[i]) == v)
+            {
+                data.remove(i);
+                return;
+            }
+        }
     }
     // -- use this function instead:
     int          size        ()      const   { return data.size(); }
@@ -180,6 +186,7 @@ public:
     void         strengthen  (Lit p);
 
 
+    void        resize  (int __size)  {data.resize(__size); }
     void pup(PUP::er &p) {
         for(int i=0; i<size(); i++)
             p|data[i];
index d3a8a3a56fa37904b65426d4712a54912b8ca79b..e3915ff0a561bafc68974d4b853d686283e5c092 100644 (file)
@@ -1,9 +1,11 @@
 c SAT07-Contest Parameters: unif2p p=7 nbc2=2803 nbc3=6541 v=3500 seed=1286605994
 c Uniform UNKNOWN (2+p)-SAT Instance nbc2=2803, nbc3=6541, p=0.70, nbv=3500, seed=1286605994
-p cnf 3 6
+p cnf 6 6
 -1 -2 0
 2 3 0
 1 3 0
 -1 2 0
 -2 0
 -1 2 1 0
+4 5 0
+5 -6 0
index 4004ca5ddc0711ae1410e768cc196e3362fca6e5..1d1ce26d6d9ffed9b679ab1b50cb97355c848373 100644 (file)
@@ -103,6 +103,107 @@ static void readClause(StreamBuffer& in, SolverState& S, CkVec<Lit>& lits) {
     }
 }
 
+/* unit propagation before real computing */
+
+static void simplify(SolverState& S)
+{
+    for(int i=0; i< S.unit_clause_index.size(); i++)
+    {
+#ifdef DEBUG
+        CkPrintf("Inside simplify before processing, unit clause number:%d, i=%d\n", S.unit_clause_index.size(), i);
+#endif
+       
+        Clause cl = S.clauses[S.unit_clause_index[i]];
+        //only one element in unit clause
+        Lit lit = cl[0];
+        S.clauses[S.unit_clause_index[i]].resize(0);
+        S.unsolved_clauses--;
+
+        int pp_ = 1;
+        int pp_i_ = 2;
+        int pp_j_ = 1;
+
+       if(toInt(lit) < 0)
+       {
+           pp_ = -1;
+           pp_i_ = 1;
+           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_];
+       
+#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++)
+       {
+           int cl_index = inClauses[j];
+#ifdef DEBUG
+           CkPrintf(" %d \n \t \t literals in this clauses: ", cl_index);
+#endif
+           Clause& cl_ = S.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;
+#ifdef DEBUG
+               CkPrintf(" %d  ", toInt(lit_));
+#endif
+               S.occurrence[abs(toInt(lit_)) - 1]--;
+               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
+               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;
+                       }
+                   }
+
+               }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;
+                       }
+                   }
+               }
+           }
+           
+           S.unsolved_clauses--;
+           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++)
+       {
+           int cl_index_ = inClauses_opposite[j];
+           Clause& cl_neg = S.clauses[cl_index_];
+           cl_neg.remove(-toInt(lit));
+           //becomes a unit clause
+           if(cl_neg.size() == 1)
+           {
+               S.unit_clause_index.push_back(cl_index_);
+           }
+       }
+
+    }
+
+    S.unit_clause_index.removeAll();
+}
+
+
 
 static void parse_confFile(gzFile input_stream, SolverState& S) {                  
     StreamBuffer in(input_stream);    
@@ -124,6 +225,7 @@ static void parse_confFile(gzFile input_stream, SolverState& S) {
                 S.var_size = vars;
                 S.occurrence.resize(vars);
                 S.positive_occurrence.resize(vars);
+                S.whichClauses.resize(2*vars);
                 for(int __i=0; __i<vars; __i++)
                 {
                     S.occurrence[__i] = 0;
@@ -142,6 +244,7 @@ static void parse_confFile(gzFile input_stream, SolverState& S) {
                 CkPrintf("conflict detected by addclauses\n");
                 CkExit();
             }
+            
         }
     
     }
@@ -175,16 +278,45 @@ Main::Main(CkArgMsg* msg)
 
     parse_confFile(in, *solver_msg);
 
+
     /*  unit propagation */ 
-    /* simplify() */
-    readfiletimer = CmiWallTimer();
+    simplify(*solver_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 ");
+    }
+
+
+    CkPrintf(" unsolved clauses %d\n", solver_msg->unsolved_clauses);
+#endif
+
+    solver_msg->unsolved_clauses = 0;
+    for(int __i=0; __i<solver_msg->clauses.size(); __i++)
+    {
+        if(solver_msg->clauses[__i].size() > 0)
+            solver_msg->unsolved_clauses++;
+    }
+    
+    readfiletimer = CmiWallTimer();
     /*fire the first chare */
     /* 1)Which variable is assigned which value this time, (variable, 1), current clauses status vector(), literal array activities */
 
     mainProxy = thisProxy;
     int max_index = get_max_element(solver_msg->occurrence);
-   
+  
+    if(max_index < 0)
+    {
+        CkPrintf(" This problem is solved by pre-processing\n");
+        CkExit();
+    }
     solver_msg->assigned_lit = Lit(max_index+1);
     solver_msg->level = 0;
     SolverState *not_msg = copy_solverstate(solver_msg);