satisfiability can be run as sequential in order to get speed up
[charm.git] / examples / charm++ / satisfiability / par_Solver.C
1 #include "main.decl.h"
2 #include "par_SolverTypes.h"
3 #include "par_Solver.h"
4 #include <map>
5 #include <vector>
6
7 #ifdef MINISAT
8 #include "Solver.h"
9 #endif
10
11 #ifdef TNM
12 #include "TNM.h"
13 #endif
14
15 using namespace std;
16
17 extern CProxy_Main mainProxy;
18 extern int grainsize;
19
20 par_SolverState::par_SolverState()
21 {
22     var_frequency = 0;
23 }
24
25
26 int par_SolverState::clausesSize()
27 {
28     return clauses.size();
29 }
30
31 void par_SolverState::attachClause(par_Clause& c)
32 {
33
34 }
35
36 int par_SolverState::unsolvedClauses()
37 {
38     int unsolved = 0;
39     for(int i=0; i< clauses.size(); i++)
40     {
41         if(clauses[i].size() > 0)
42             unsolved++;
43     }
44
45     return unsolved;
46 }
47
48 void par_SolverState::printSolution()
49 {
50     for(int _i=0; _i<var_size; _i++)
51     {
52         CkPrintf("%d\n", occurrence[_i]);
53     }
54  
55 }
56
57 /* add clause, before adding, check unit conflict */
58 bool par_SolverState::addClause(CkVec<par_Lit>& ps)
59 {
60     /*TODO precheck is needed here */
61     if(ps.size() == 1)//unit clause
62     {
63         for(int _i=0; _i<unit_clause_index.size(); _i++)
64         {
65             int index = unit_clause_index[_i];
66
67             par_Clause unit = clauses[index];
68             par_Lit     unit_lit = unit[0];
69
70             if(unit_lit == ~ps[0])
71             {
72    
73                 CkPrintf("clause conflict between %d and %d\n", index, clauses.size());
74                 return false;
75             }
76         }
77        /* all unit clauses are checked, no repeat, no conflict */
78         unit_clause_index.push_back(clauses.size());
79     }else{
80     //check whether the clause is already satisfiable in any case
81     /* if x and ~x exist in the same clause, this clause is already satisfiable, we do not have to deal with it */
82    
83     for(int i=0; i< ps.size(); i++)
84     {
85         par_Lit lit = ps[i];
86
87         for(int j=0; j<i; j++)
88         {
89             if(lit == ~ps[j])
90             {
91                 CkPrintf("This clause is already satisfiable\n");
92                 for(int _i=0; _i<ps.size(); _i++)
93                 {
94                    occurrence[abs(toInt(ps[_i])-1)]--; 
95                    if(toInt(ps[_i]) > 0)
96                        positive_occurrence[abs(toInt(ps[_i])-1)]--; 
97                 }
98                 return true;
99             }
100         }
101     }
102     }
103     clauses.push_back(par_Clause());
104     clauses[clauses.size()-1].attachdata(ps, false);
105     // build the linklist for each literal pointing to the clause, where the literal occurs
106     for(int i=0; i< ps.size(); i++)
107     {
108         par_Lit lit = ps[i];
109
110         if(toInt(lit) > 0)
111             whichClauses[2*toInt(lit)-2].push_back(clauses.size()-1);
112         else
113             whichClauses[-2*toInt(lit)-1].push_back(clauses.size()-1);
114
115     }
116
117     return true;
118 }
119
120 void par_SolverState::assignclause(CkVec<par_Clause>& cls )
121 {
122     clauses.removeAll();
123     for(int i=0; i<cls.size(); i++)
124     {
125         clauses.push_back( cls[i]);
126     }
127 }
128
129 /* *********** Solver chare */
130
131 mySolver::mySolver(par_SolverState* state_msg)
132 {
133
134     /* Which variable get assigned  */
135     par_Lit lit = state_msg->assigned_lit;
136 #ifdef DEBUG    
137     CkPrintf("\n\nNew chare: literal = %d, occurrence size=%d, level=%d \n", toInt(lit), state_msg->occurrence.size(), state_msg->level);
138 #endif    
139     par_SolverState *next_state = copy_solverstate(state_msg);
140
141     //Unit clauses
142     /* use this value to propagate the clauses */
143     // deal with the clauses where this literal is
144     int _unit_ = -1;
145     while(1){
146         int pp_ = 1;
147         int pp_i_ = 2;
148         int pp_j_ = 1;
149
150         if(toInt(lit) < 0)
151         {
152             pp_ = -1;
153             pp_i_ = 1;
154             pp_j_ = 2;
155         }
156
157         next_state->occurrence[pp_*toInt(lit)-1] = -pp_i_;
158     
159         //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());
160
161         CkVec<int> &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
162         CkVec<int> &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
163
164     // literal with same sign, remove all these clauses
165        for(int j=0; j<inClauses.size(); j++)
166        {
167            int cl_index = inClauses[j];
168
169            par_Clause& cl_ = next_state->clauses[cl_index];
170            //for all the literals in this clauses, the occurrence decreases by 1
171            for(int k=0; k< cl_.size(); k++)
172            {
173                par_Lit lit_ = cl_[k];
174                if(toInt(lit_) == toInt(lit))
175                    continue;
176                next_state->occurrence[abs(toInt(lit_)) - 1]--;
177                if(toInt(lit_) > 0)
178                {
179                    next_state->positive_occurrence[toInt(lit_)-1]--;
180                    //remove the clause index for the literal
181                    for(int _i = 0; _i<next_state->whichClauses[2*toInt(lit_)-2].size(); _i++)
182                    {
183                        if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
184                        {
185                            next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
186                            break;
187                        }
188                    }
189                }else
190                {
191                    for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
192                    {
193                        if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
194                        {
195                            next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
196                            break;
197                        }
198                    }
199                }
200            } //finish dealing with all literal in the clause
201            next_state->clauses[cl_index].resize(0);
202        } //finish dealing with clauses where the literal occur the same
203        /* opposite to the literal */
204        for(int j=0; j<inClauses_opposite.size(); j++)
205        {
206            int cl_index_ = inClauses_opposite[j];
207            par_Clause& cl_neg = next_state->clauses[cl_index_];
208            cl_neg.remove(-toInt(lit));
209
210            /*becomes a unit clause */
211            if(cl_neg.size() == 1)
212            {
213                next_state->unit_clause_index.push_back(cl_index_);
214            }else if (cl_neg.size() == 0)
215            {
216                return;
217            }
218        }
219
220        _unit_++;
221        if(_unit_ == next_state->unit_clause_index.size())
222            break;
223        par_Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
224
225        while(cl.size() == 0){
226            _unit_++;
227            if(_unit_ == next_state->unit_clause_index.size())
228                break;
229            cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
230        };
231
232        if(_unit_ == next_state->unit_clause_index.size())
233            break;
234        lit = cl[0];
235
236
237     }
238     /***************/
239
240     int unsolved = next_state->unsolvedClauses();
241     if(unsolved == 0)
242     {
243         CkPrintf("One solution found in parallel processing \n");
244         //next_state->printSolution();
245         mainProxy.done(next_state->occurrence);
246         return;
247     }
248     int max_index = get_max_element(next_state->occurrence);
249 #ifdef DEBUG
250     CkPrintf("max index = %d\n", max_index);
251 #endif
252     //if() left literal unassigned is larger than a grain size, parallel 
253     ///* When we start sequential 3SAT Grainsize problem*/
254    
255     /* the other branch */
256     par_SolverState *new_msg2 = copy_solverstate(next_state);;
257
258     next_state->level = state_msg->level+1;
259
260     int lower = state_msg->lower;
261     int higher = state_msg->higher;
262     int middle = (lower+higher)/2;
263     int positive_max = next_state->positive_occurrence[max_index];
264     if(positive_max >= next_state->occurrence[max_index] - positive_max)
265     {
266         next_state->assigned_lit = par_Lit(max_index+1);
267         next_state->occurrence[max_index] = -2;
268     }
269     else
270     {
271         next_state->assigned_lit = par_Lit(-max_index-1);
272         next_state->occurrence[max_index] = -1;
273     }
274     bool satisfiable_1 = true;
275
276     if(unsolved > grainsize)
277     {
278         next_state->lower = lower + 1;
279         next_state->higher = middle;
280         *((int *)CkPriorityPtr(next_state)) = lower+1;
281         CkSetQueueing(next_state, CK_QUEUEING_IFIFO);
282         CProxy_mySolver::ckNew(next_state);
283     }
284     else //sequential
285     {
286         /* This code is urgly. Need to revise it later. Convert par data structure to sequential 
287          */
288         vector< vector<int> > seq_clauses;
289         //seq_clauses.resize(next_state->clauses.size());
290         for(int _i_=0; _i_<next_state->clauses.size(); _i_++)
291         {
292             if(next_state->clauses[_i_].size() > 0)
293             {
294                 vector<int> unsolvedclaus;
295                 par_Clause& cl = next_state->clauses[_i_];
296                 unsolvedclaus.resize(cl.size());
297                 for(int _j_=0; _j_<cl.size(); _j_++)
298                 {
299                     unsolvedclaus[_j_] = toInt(cl[_j_]);
300                 }
301                 seq_clauses.push_back(unsolvedclaus);
302             }
303         }
304         satisfiable_1 = seq_processing(next_state->var_size, seq_clauses);//seq_solve(next_state);
305         if(satisfiable_1)
306         {
307             CkPrintf("One solution found by sequential processing \n");
308             mainProxy.done(next_state->occurrence);
309             return;
310         }
311     }
312
313     new_msg2->level = state_msg->level+1;
314     if(positive_max >= new_msg2->occurrence[max_index] - positive_max)
315     {
316         new_msg2->assigned_lit = par_Lit(-max_index-1);
317         new_msg2->occurrence[max_index] = -1;
318     }
319     else
320     {
321         new_msg2->assigned_lit = par_Lit(max_index+1);
322         new_msg2->occurrence[max_index] = -2;
323     }
324     unsolved = new_msg2->unsolvedClauses();
325     if(unsolved > grainsize)
326     {
327         new_msg2->lower = middle + 1;
328         new_msg2->higher = higher-1;
329         *((int *)CkPriorityPtr(new_msg2)) = middle+1;
330         CkSetQueueing(new_msg2, CK_QUEUEING_IFIFO);
331         CProxy_mySolver::ckNew(new_msg2);
332     }
333     else
334     {
335        
336         vector< vector<int> > seq_clauses;
337         for(int _i_=0; _i_<new_msg2->clauses.size(); _i_++)
338         {
339             par_Clause& cl = new_msg2->clauses[_i_];
340             if(cl.size() > 0)
341             {
342                 vector<int> unsolvedclaus;
343                 unsolvedclaus.resize(cl.size());
344                 for(int _j_=0; _j_<cl.size(); _j_++)
345                 {
346                     unsolvedclaus[_j_] = toInt(cl[_j_]);
347                 }
348                 seq_clauses.push_back(unsolvedclaus);
349             }
350         }
351
352         bool ret = seq_processing(new_msg2->var_size,  seq_clauses);//seq_solve(next_state);
353         //bool ret = Solver::seq_processing(new_msg2->clauses);//seq_solve(new_msg2);
354         if(ret)
355         {
356             CkPrintf("One solution found by sequential processing \n");
357             mainProxy.done(new_msg2->occurrence);
358         }
359         return;
360     }
361
362 }
363
364 /* Which literals are already assigned, which is assigned this interation, the unsolved clauses */
365 /* should all these be passed as function parameters */
366 /* solve the 3sat in sequence */
367
368 long long int computes = 0;
369 bool mySolver::seq_solve(par_SolverState* state_msg)
370 {
371     /* Which variable get assigned  */
372     par_Lit lit = state_msg->assigned_lit;
373        
374 #ifdef DEBUG
375     CkPrintf("\n\n Computes=%d Sequential SAT New chare: literal = %d,  level=%d, unsolved clauses=%d\n", computes++, toInt(assigned_var), state_msg->level, state_msg->clauses.size());
376     //CkPrintf("\n\n Computes=%d Sequential SAT New chare: literal = %d, occurrence size=%d, level=%d \n", computes++, toInt(assigned_var), state_msg->occurrence.size(), state_msg->level);
377 #endif
378     par_SolverState *next_state = copy_solverstate(state_msg);
379     
380     //Unit clauses
381     /* use this value to propagate the clauses */
382 #ifdef DEBUG
383     CkPrintf(" remainning clause size is %d\n", (state_msg->clauses).size());
384 #endif
385
386     int _unit_ = -1;
387     while(1){
388     int pp_ = 1;
389     int pp_i_ = 2;
390     int pp_j_ = 1;
391
392     if(toInt(lit) < 0)
393     {
394         pp_ = -1;
395         pp_i_ = 1;
396         pp_j_ = 2;
397     }
398
399     next_state->occurrence[pp_*toInt(lit)-1] = -pp_i_;
400     
401     CkVec<int> &inClauses = next_state->whichClauses[pp_*2*toInt(lit)-pp_i_];
402     CkVec<int> &inClauses_opposite = next_state->whichClauses[pp_*2*toInt(lit)-pp_j_];
403
404     // literal with same sign, remove all these clauses
405     for(int j=0; j<inClauses.size(); j++)
406     {
407         int cl_index = inClauses[j];
408
409         par_Clause& cl_ = next_state->clauses[cl_index];
410         //for all the literals in this clauses, the occurrence decreases by 1
411         for(int k=0; k< cl_.size(); k++)
412         {
413             par_Lit lit_ = cl_[k];
414             if(toInt(lit_) == toInt(lit))
415                 continue;
416             next_state->occurrence[abs(toInt(lit_)) - 1]--;
417             if(toInt(lit_) > 0)
418             {
419                 next_state->positive_occurrence[toInt(lit_)-1]--;
420                 //remove the clause index for the literal
421                 for(int _i = 0; _i<next_state->whichClauses[2*toInt(lit_)-2].size(); _i++)
422                 {
423                     if(next_state->whichClauses[2*toInt(lit_)-2][_i] == cl_index)
424                     {
425                         next_state->whichClauses[2*toInt(lit_)-2].remove(_i);
426                         break;
427                     }
428                 }
429             }else
430             {
431                 for(int _i = 0; _i<next_state->whichClauses[-2*toInt(lit_)-1].size(); _i++)
432                 {
433                     if(next_state->whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
434                     {
435                         next_state->whichClauses[-2*toInt(lit_)-1].remove(_i);
436                         break;
437                     }
438                 }
439             }
440         }
441             next_state->clauses[cl_index].resize(0);
442     }
443    
444     for(int j=0; j<inClauses_opposite.size(); j++)
445     {
446         int cl_index_ = inClauses_opposite[j];
447         par_Clause& cl_neg = next_state->clauses[cl_index_];
448         cl_neg.remove(-toInt(lit));
449             //becomes a unit clause
450          if(cl_neg.size() == 1)
451          {
452              next_state->unit_clause_index.push_back(cl_index_);
453          }else if (cl_neg.size() == 0)
454          {
455                 return false;
456          }
457     }
458    
459     _unit_++;
460     if(_unit_ == next_state->unit_clause_index.size())
461         break;
462     par_Clause cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
463     
464     while(cl.size() == 0){
465         _unit_++;
466         if(_unit_ == next_state->unit_clause_index.size())
467             break;
468         cl = next_state->clauses[next_state->unit_clause_index[_unit_]];
469         
470     };
471
472     if(_unit_ == next_state->unit_clause_index.size())
473         break;
474     
475     lit = cl[0];
476     }
477    
478     int unsolved = next_state->unsolvedClauses();
479     if(unsolved == 0)
480     {
481         CkPrintf("One solution found in sequential processing, check the output file for assignment\n");
482         mainProxy.done(next_state->occurrence);
483         return true;
484     }
485     
486     /**********************/
487     
488         /* it would be better to insert the unit literal in order of their occurrence */
489         /* make a decision and then fire new tasks */
490         /* if there is unit clause, should choose these first??? TODO */
491         /* TODO which variable to pick up */
492         /*unit clause literal and also which occurrs most times */
493         int max_index =  get_max_element(next_state->occurrence);
494 #ifdef DEBUG
495         CkPrintf("max index = %d\n", max_index);
496 #endif
497         next_state->level = state_msg->level+1;
498
499         par_SolverState *new_msg2 = copy_solverstate(next_state);;
500         
501         int positive_max = next_state->positive_occurrence[max_index];
502         if(positive_max >= next_state->occurrence[max_index] - positive_max)
503         {
504             next_state->occurrence[max_index] = -2;
505             next_state->assigned_lit = par_Lit(max_index+1);
506         }
507         else
508         {
509             next_state->occurrence[max_index] = -1;
510             next_state->assigned_lit = par_Lit(-max_index-1);
511         } 
512
513         bool   satisfiable_1 = seq_solve(next_state);
514         if(satisfiable_1)
515         {
516             return true;
517         }
518         
519         new_msg2->level = state_msg->level+1;
520        
521         if(positive_max >= next_state->occurrence[max_index] - positive_max)
522         {
523             new_msg2->occurrence[max_index] = -1;
524             new_msg2->assigned_lit = par_Lit(-max_index-1);
525         }
526         else
527         {
528             new_msg2->occurrence[max_index] = -2;
529             new_msg2->assigned_lit = par_Lit(max_index+1);
530         } 
531             
532         bool satisfiable_0 = seq_solve(new_msg2);
533         if(satisfiable_0)
534         {
535             return true;
536         }
537
538         //CkPrintf("Unsatisfiable through sequential\n");
539         return false;
540
541 }