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