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