satisfiability can be run as sequential in order to get speed up
[charm.git] / examples / charm++ / satisfiability / main.C
1 #include <stdio.h>
2 #include <cstring>
3 #include <stdint.h>
4 #include <errno.h>
5 #include <limits.h>
6
7 #include <signal.h>
8 #include <zlib.h>
9
10 #include <vector>
11
12 #include "main.decl.h"
13 #include "main.h"
14
15 #include "par_SolverTypes.h"
16 #include "par_Solver.h"
17
18 #ifdef MINISAT
19 #include "Solver.h"
20 #endif
21
22 #ifdef TNM
23 #include "TNM.h"
24 #endif
25
26 using namespace std;
27
28 //#include "util.h"
29
30 CProxy_Main mainProxy;
31
32 #define CHUNK_LIMIT 1048576
33
34 char inputfile[50];
35
36 class StreamBuffer {
37     gzFile  in;
38     char    buf[CHUNK_LIMIT];
39     int     pos;
40     int     size;
41
42     void assureLookahead() {
43         if (pos >= size) {
44             pos  = 0;
45             size = gzread(in, buf, sizeof(buf)); } }
46
47 public:
48             StreamBuffer(gzFile i) : in(i), pos(0), size(0) {
49                 assureLookahead(); }
50
51             int  operator *  () { return (pos >= size) ? EOF : buf[pos]; }
52             void operator ++ () { pos++; assureLookahead(); }
53 };
54
55 static bool match(StreamBuffer& in, char* str) {
56     for (; *str != 0; ++str, ++in)
57         if (*str != *in)
58             return false;
59     return true;
60 }
61
62
63 void error_exit(char *error)
64 {
65     printf("%s\n", error);
66     CkExit();
67 }
68
69 void skipWhitespace(StreamBuffer& in) 
70 {
71     while ((*in >= 9 && *in <= 13) || *in == 32)
72         ++in;
73 }
74
75 void skipLine(StreamBuffer& in) {
76     for (;;){
77         if (*in == EOF || *in == '\0') return;
78         if (*in == '\n')
79         { ++in; return; }
80         ++in;
81     } 
82 }
83
84
85 int parseInt(StreamBuffer& in) {
86     int     val = 0;
87     bool    neg = false;
88     skipWhitespace(in);
89     if      (*in == '-') neg = true, ++in;
90     else if (*in == '+') ++in;
91     if (*in < '0' || *in > '9')
92         error_exit((char*)"ParseInt error\n");
93
94     while (*in >= '0' && *in <= '9')
95     {
96         val = val*10 + (*in - '0');
97         ++in;
98     }
99     return neg ? -val : val; 
100 }
101
102 static void readClause(StreamBuffer& in, par_SolverState& S, CkVec<par_Lit>& lits) {
103     int     parsed_lit, var;
104     lits.removeAll();
105     for (;;){
106         parsed_lit = parseInt(in);
107         if (parsed_lit == 0) break;
108         var = abs(parsed_lit)-1;
109         
110         S.occurrence[var]++;
111         if(parsed_lit>0)
112             S.positive_occurrence[var]++;
113         lits.push_back( par_Lit(parsed_lit));
114     }
115 }
116
117 /* unit propagation before real computing */
118
119 static void simplify(par_SolverState& S)
120 {
121     for(int i=0; i< S.unit_clause_index.size(); i++)
122     {
123 #ifdef DEBUG
124         CkPrintf("Inside simplify before processing, unit clause number:%d, i=%d\n", S.unit_clause_index.size(), i);
125 #endif
126        
127         par_Clause cl = S.clauses[S.unit_clause_index[i]];
128         //only one element in unit clause
129         par_Lit lit = cl[0];
130         S.clauses[S.unit_clause_index[i]].resize(0);
131
132         int pp_ = 1;
133         int pp_i_ = 2;
134         int pp_j_ = 1;
135
136        if(toInt(lit) < 0)
137        {
138            pp_ = -1;
139            pp_i_ = 1;
140            pp_j_ = 2;
141        }
142        S.occurrence[pp_*toInt(lit)-1] = -pp_i_;
143        CkVec<int> &inClauses = S.whichClauses[pp_*2*toInt(lit)-pp_i_];
144        CkVec<int> &inClauses_opposite = S.whichClauses[pp_*2*toInt(lit)-pp_j_];
145        
146        // literal with same sign
147        for(int j=0; j<inClauses.size(); j++)
148        {
149            int cl_index = inClauses[j];
150 #ifdef DEBUG
151            CkPrintf(" %d \n \t \t literals in this clauses: ", cl_index);
152 #endif
153            par_Clause& cl_ = S.clauses[cl_index];
154            //for all the literals in this clauses, the occurrence decreases by 1
155            for(int k=0; k< cl_.size(); k++)
156            {
157                par_Lit lit_ = cl_[k];
158                if(toInt(lit_) == toInt(lit))
159                    continue;
160 #ifdef DEBUG
161                CkPrintf(" %d  ", toInt(lit_));
162 #endif
163                S.occurrence[abs(toInt(lit_)) - 1]--;
164                if(toInt(lit_) > 0)
165                {
166                    S.positive_occurrence[toInt(lit_)-1]--;
167                    //S.whichClauses[2*toInt(lit_)-2].remove(cl_index);
168                 //remove the clause index for the literal
169                     /* Low effieciency */
170                    for(int _i = 0; _i<S.whichClauses[2*toInt(lit_)-2].size(); _i++)
171                    {
172                        if(S.whichClauses[2*toInt(lit_)-2][_i] == cl_index)
173                        {
174                            S.whichClauses[2*toInt(lit_)-2].remove(_i);
175                             break;
176                        }
177                    }
178
179                }else
180                {
181                    for(int _i = 0; _i<S.whichClauses[-2*toInt(lit_)-1].size(); _i++)
182                    {
183                        if(S.whichClauses[-2*toInt(lit_)-1][_i] == cl_index)
184                        {
185                            S.whichClauses[-2*toInt(lit_)-1].remove(_i);
186                            break;
187                        }
188                    }
189                }
190            }
191            
192            S.clauses[cl_index].resize(0); //this clause goes away. In order to keep index unchanged, resize it as 0
193        }
194        
195        for(int j=0; j<inClauses_opposite.size(); j++)
196        {
197            int cl_index_ = inClauses_opposite[j];
198            par_Clause& cl_neg = S.clauses[cl_index_];
199            cl_neg.remove(-toInt(lit));
200            //becomes a unit clause
201            if(cl_neg.size() == 1)
202            {
203                S.unit_clause_index.push_back(cl_index_);
204            }
205        }
206
207     }
208
209     S.unit_clause_index.removeAll();
210 }
211
212
213
214 static void parse_confFile(gzFile input_stream, par_SolverState& S) {                  
215     StreamBuffer in(input_stream);    
216       CkVec<par_Lit> lits;                                                 
217     int i  = 0;
218     
219     for (;;){                                                      
220         //printf(" + on %d\n", i++);
221         skipWhitespace(in);                                        
222         if (*in == EOF)                                            
223             break;                                                 
224         else if (*in == 'p'){                                      
225             if (match(in, (char*)"p cnf")){                               
226                 int vars    = parseInt(in);                        
227                 int clauses = parseInt(in);                        
228                 printf("|  Number of variables:  %-12d                                         |\n", vars);
229                 printf("|  Number of clauses:    %-12d                                         |\n", clauses);
230                 
231
232                 S.var_size = vars;
233                 S.occurrence.resize(vars);
234                 S.positive_occurrence.resize(vars);
235                 S.whichClauses.resize(2*vars);
236                 for(int __i=0; __i<vars; __i++)
237                 {
238                     S.occurrence[__i] = 0;
239                     S.positive_occurrence[__i] = 0;
240                 }
241             }else{
242                 printf("PARSE ERROR! Unexpected char: %c\n", *in);
243                 error_exit((char*)"Parse Error\n");
244             }
245         } else if (*in == 'c' || *in == 'p')
246             skipLine(in);
247         else{
248             readClause(in, S, lits);
249             if( !S.addClause(lits))
250             {
251                 CkPrintf("conflict detected by addclauses\n");
252                 CkExit();
253             }
254             
255         }
256     
257     }
258 }
259
260
261 Main::Main(CkArgMsg* msg)
262 {
263
264     grainsize = 1;
265     par_SolverState* solver_msg = new (8 * sizeof(int))par_SolverState;
266     if(msg->argc < 2)
267     {
268         error_exit((char*)"Usage: sat filename grainsize\n");
269     }else
270         grainsize = atoi(msg->argv[2]);
271
272
273     CkPrintf("problem file:\t\t%s\ngrainsize:\t\t%d\nprocessor number:\t\t%d\n", msg->argv[1], grainsize, CkNumPes()); 
274
275     /* read file */
276
277     starttimer = CmiWallTimer();
278
279     /*read information from file */
280     gzFile in = gzopen(msg->argv[1], "rb");
281
282     strcpy(inputfile, msg->argv[1]);
283
284     if(in == NULL)
285     {
286         error_exit((char*)"Invalid input filename\n");
287     }
288
289     parse_confFile(in, *solver_msg);
290
291     /*  unit propagation */ 
292     simplify(*solver_msg);
293 #ifdef DEBUG
294     for(int __i = 0; __i<solver_msg->occurrence.size(); __i++)
295     {
296         FILE *file;
297         char outputfile[50];
298         sprintf(outputfile, "%s.sat", inputfile);
299         file = fopen(outputfile, "w");
300         for(int i=0; i<assignment.size(); i++)
301         {
302             fprintf(file, "%d\n", assignment[i]);
303         }
304     }
305
306 #endif
307
308     int unsolved = solver_msg->unsolvedClauses();
309
310     if(unsolved == 0)
311     {
312         CkPrintf(" This problem is solved by pre-processing\n");
313         CkExit();
314     }
315     readfiletimer = CmiWallTimer();
316     /*fire the first chare */
317     /* 1)Which variable is assigned which value this time, (variable, 1), current clauses status vector(), literal array activities */
318
319
320     /***  If grain size is larger than the clauses size, that means 'sequential' */
321     if(grainsize > solver_msg->clauses.size())
322     {
323         vector< vector<int> > seq_clauses;
324         for(int _i_=0; _i_<solver_msg->clauses.size(); _i_++)
325         {
326             if(solver_msg->clauses[_i_].size() > 0)
327             {
328                 vector<int> unsolvedclaus;
329                 par_Clause& cl = solver_msg->clauses[_i_];
330                 unsolvedclaus.resize(cl.size());
331                 for(int _j_=0; _j_<cl.size(); _j_++)
332                 {
333                     unsolvedclaus[_j_] = toInt(cl[_j_]);
334                 }
335                 seq_clauses.push_back(unsolvedclaus);
336             }
337         }
338         bool satisfiable_1 = seq_processing(solver_msg->var_size, seq_clauses);//seq_solve(next_state);
339
340         if(satisfiable_1)
341         {
342             CkPrintf("One solution found without using any parallel\n");
343         }else
344         {
345        
346             CkPrintf(" Unsatisfiable\n");
347         }
348         done(solver_msg->occurrence);
349         return;
350     }
351     mainProxy = thisProxy;
352     int max_index = get_max_element(solver_msg->occurrence);
353     
354     solver_msg->assigned_lit = par_Lit(max_index+1);
355     solver_msg->level = 0;
356     par_SolverState *not_msg = copy_solverstate(solver_msg);
357     
358     solver_msg->occurrence[max_index] = -2;
359     not_msg->assigned_lit = par_Lit(-max_index-1);
360     not_msg->occurrence[max_index] = -1;
361     
362     int positive_max = solver_msg->positive_occurrence[max_index];
363     if(positive_max >= solver_msg->occurrence[max_index] - positive_max)
364     {
365
366         // assign true first and then false
367         *((int *)CkPriorityPtr(solver_msg)) = INT_MIN;
368         CkSetQueueing(solver_msg, CK_QUEUEING_IFIFO);
369         solver_msg->lower = INT_MIN;
370         solver_msg->higher = 0;
371         CProxy_mySolver::ckNew(solver_msg);
372         
373         *((int *)CkPriorityPtr(not_msg)) = 0;
374         CkSetQueueing(not_msg, CK_QUEUEING_IFIFO);
375         not_msg->lower = 0;
376         not_msg->higher = INT_MAX;
377         CProxy_mySolver::ckNew(not_msg);
378     }else
379     {
380         *((int *)CkPriorityPtr(not_msg)) = INT_MIN;
381         CkSetQueueing(not_msg, CK_QUEUEING_IFIFO);
382         not_msg->lower = INT_MIN;
383         not_msg->higher = 0;
384         CProxy_mySolver::ckNew(not_msg);
385         
386         *((int *)CkPriorityPtr(solver_msg)) = 0;
387         CkSetQueueing(solver_msg, CK_QUEUEING_IFIFO);
388         solver_msg->lower = 0;
389         solver_msg->higher = INT_MAX;
390         CProxy_mySolver::ckNew(solver_msg);
391
392     }
393 }
394
395 Main::Main(CkMigrateMessage* msg) {}
396
397 void Main::done(CkVec<int> assignment)
398 {
399
400     double endtimer = CmiWallTimer();
401
402     CkPrintf("\nFile reading and processing time:         %f\n", readfiletimer-starttimer);
403     CkPrintf("Solving time:                             %f\n", endtimer - readfiletimer);
404  
405     /*
406     FILE *file;
407     char outputfile[50];
408     sprintf(outputfile, "%s.sat", inputfile);
409     file = fopen(outputfile, "w");
410
411     for(int i=0; i<assignment.size(); i++)
412     {
413         fprintf(file, "%d\n", assignment[i]);
414     }
415     */
416     CkExit();
417 }
418 #include "main.def.h"
419