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