add minisat and TNM sequential solvers in sat problem
[charm.git] / examples / charm++ / satisfiability / TNM / inputbis.C
1 \r
2 #define OLD_CLAUSE_REDUNDANT -77\r
3 #define NEW_CLAUSE_REDUNDANT -7\r
4 \r
5 \r
6 int smaller_than(int lit1, int lit2) {\r
7   return ((lit1<NB_VAR) ? lit1 : lit1-NB_VAR) < \r
8     ((lit2<NB_VAR) ? lit2 : lit2-NB_VAR);\r
9 }\r
10 \r
11 my_type redundant(int *new_clause, int *old_clause) {\r
12   int lit1, lit2, old_clause_diff=0, new_clause_diff=0;\r
13     \r
14   lit1=*old_clause; lit2=*new_clause;\r
15   while ((lit1 != NONE) && (lit2 != NONE)) {\r
16     if (smaller_than(lit1, lit2)) {\r
17       lit1=*(++old_clause); old_clause_diff++;\r
18     }\r
19     else\r
20       if (smaller_than(lit2, lit1)) {\r
21         lit2=*(++new_clause); new_clause_diff++;\r
22       }\r
23       else\r
24         if (complement(lit1, lit2)) {\r
25           return FALSE; /* old_clause_diff++; new_clause_diff++; j1++; j2++; */\r
26         }\r
27         else {\r
28           lit1=*(++old_clause);  lit2=*(++new_clause);\r
29         }\r
30   }\r
31   if ((lit1 == NONE) && (old_clause_diff == 0))\r
32     /* la nouvelle clause est redondante ou subsumee */\r
33     return NEW_CLAUSE_REDUNDANT;\r
34   if ((lit2 == NONE) && (new_clause_diff == 0))\r
35     /* la old clause est redondante ou subsumee */\r
36     return OLD_CLAUSE_REDUNDANT;\r
37   return FALSE;\r
38 }\r
39 \r
40 my_type get_resolvant(int *clause1, int *clause2, int *resolvant) {\r
41   int lit1, lit2, nb_diff1=0,  nb_diff2=0,\r
42     nb_iden=0, nb_opps=0, j1=0, j2=0, j, limited_length;\r
43 \r
44   while (((lit1=clause1[j1])!=NONE) && ((lit2=clause2[j2]) != NONE)) {\r
45     if (complement(lit1, lit2)) {\r
46       j1++; j2++; nb_opps++;\r
47     }\r
48     else\r
49       if (lit1 == lit2) {\r
50         j1++; j2++; nb_iden++;\r
51       }\r
52       else\r
53         if (smaller_than(lit1, lit2)) {\r
54           nb_diff1++; j1++;\r
55         }\r
56         else {\r
57           nb_diff2++; j2++;\r
58         }\r
59   }\r
60   if (nb_opps ==1) {\r
61     if (clause1[j1] ==NONE) {\r
62       for (; clause2[j2]!= NONE; j2++) nb_diff2++;\r
63     }\r
64     else {\r
65       for (; clause1[j1]!= NONE; j1++) nb_diff1++;\r
66     }\r
67     if ((j1==1) || (j2==1))  limited_length=RESOLVANT_LENGTH; \r
68     else\r
69       if ((j1==2) && (j2==2))  limited_length=1;\r
70       else\r
71         if (j1<j2) limited_length=((j1<RESOLVANT_LENGTH) ? j1 : RESOLVANT_LENGTH);\r
72         else  limited_length=((j2<RESOLVANT_LENGTH) ? j2 : RESOLVANT_LENGTH);\r
73 \r
74     if (nb_diff1 + nb_diff2 + nb_iden <= limited_length) {\r
75       j1=0; j2=0; j=0;\r
76       while (((lit1 = clause1[j1])!=NONE) && ((lit2 = clause2[j2]) != NONE)) {\r
77         if (lit1 == lit2) {\r
78           resolvant[j] = lit1; j1++; j2++; j++;\r
79         }\r
80         else \r
81           if (smaller_than(lit1, lit2)) {\r
82             resolvant[j] = lit1; j1++; j++;\r
83           }\r
84           else\r
85             if (smaller_than(lit2, lit1)) {\r
86               resolvant[j] = lit2; j2++; j++;\r
87             }\r
88             else {\r
89               j1++; j2++;\r
90             }\r
91       }\r
92       if (clause1[j1] ==NONE) while ((resolvant[j++] = clause2[j2++]) != NONE);\r
93       else while ((resolvant[j++] = clause1[j1++]) != NONE);\r
94       if (j==0) return NONE;\r
95       if (nb_diff2==0) return 2; /* clause1 is redundant */\r
96       return TRUE;\r
97     }\r
98   }\r
99   return FALSE;\r
100 }\r
101 \r
102 int INVOLVED_CLAUSE_STACK[tab_clause_size];\r
103 int INVOLVED_CLAUSE_STACK_fill_pointer=0;\r
104 int CLAUSE_INVOLVED[tab_clause_size];\r
105 \r
106 void remove_passive_clauses() {\r
107   int  clause, put_in, first=NONE;\r
108   for (clause=0; clause<NB_CLAUSE; clause++) {\r
109     if (clause_state[clause]==PASSIVE) {\r
110       first=clause; break;\r
111     }\r
112   }\r
113   if (first!=NONE) {\r
114     put_in=first;\r
115     for(clause=first+1; clause<NB_CLAUSE; clause++) {\r
116       if (clause_state[clause]==ACTIVE) {\r
117         sat[put_in]=sat[clause]; var_sign[put_in]=var_sign[clause];\r
118         clause_state[put_in]=ACTIVE; \r
119         clause_length[put_in]=clause_length[clause];\r
120         put_in++;\r
121       }\r
122     }\r
123     NB_CLAUSE=put_in;\r
124   }\r
125 }\r
126 \r
127 void remove_passive_vars_in_clause(int clause) {\r
128   int *vars_signs, *vars_signs1, var, var1, first=NONE;\r
129   vars_signs=var_sign[clause];\r
130   for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {\r
131     if (var_state[var]!=ACTIVE) {\r
132       first=var; break;\r
133     }\r
134   }\r
135   if (first!=NONE) {\r
136     for(vars_signs1=vars_signs+2, var1=*vars_signs1; var1!=NONE; \r
137         var1=*(vars_signs1+=2)) {\r
138       if (var_state[var1]==ACTIVE) {\r
139         *vars_signs=var1; *(vars_signs+1) = *(vars_signs1+1);\r
140         vars_signs+=2;\r
141       }\r
142     }\r
143     *vars_signs=NONE;\r
144   }\r
145 }\r
146 \r
147 int clean_structure() {\r
148   int clause, var, *vars_signs;\r
149   remove_passive_clauses();\r
150   if (NB_CLAUSE==0) \r
151     return SATISFIABLE;\r
152   for (clause=0; clause<NB_CLAUSE; clause++) \r
153     remove_passive_vars_in_clause(clause);\r
154   NB_ACTIVE_VAR=0;\r
155   for (var=0; var<NB_VAR; var++) { \r
156     neg_nb[var] = 0;\r
157     pos_nb[var] = 0;\r
158     if (var_state[var]==ACTIVE) NB_ACTIVE_VAR++;\r
159   }\r
160   for (clause=0; clause<NB_CLAUSE; clause++) {\r
161     vars_signs=var_sign[clause];\r
162     for(var=*vars_signs; var!=NONE; var=*(vars_signs+=2)) {\r
163       if (*(vars_signs+1)==POSITIVE) \r
164         pos_in[var][pos_nb[var]++]=clause;\r
165       else  neg_in[var][neg_nb[var]++]=clause;\r
166     }\r
167   }\r
168   for (var=0; var<NB_VAR; var++) { \r
169     neg_in[var][neg_nb[var]]=NONE;\r
170     pos_in[var][pos_nb[var]]=NONE;\r
171   }\r
172   return TRUE;\r
173 }\r
174 \r
175 int unitclause_process();\r
176 int simplify_formula();\r
177 \r
178 int lire_clauses(const vector< vector<int> >& _clauses) {\r
179     int i, j, jj, ii, length, tautologie, lits[1000], lit, lit1;\r
180     for (i=0; i<NB_CLAUSE; i++) {\r
181     \r
182         length = _clauses[i].size();\r
183         for(j=0; j<length; j++)\r
184         {\r
185             lits[j] = _clauses[i][j];\r
186         }\r
187         tautologie = FALSE;\r
188         /* test if some literals are redundant and sort the clause */\r
189         for (ii=0; ii<length-1; ii++) {\r
190             lit = lits[ii];\r
191             for (jj=ii+1; jj<length; jj++) {\r
192                 if (abs(lit)>abs(lits[jj])) {\r
193                     lit1=lits[jj]; lits[jj]=lit; lit=lit1;\r
194                 }\r
195                 else\r
196                     if (lit == lits[jj]) {\r
197                         lits[jj] = lits[length-1]; \r
198                         jj--; length--; lits[length] = 0;\r
199                     }\r
200                     else\r
201                         if (abs(lit) == abs(lits[jj])) {\r
202                             tautologie = TRUE; break;\r
203                         }\r
204             }\r
205             if (tautologie == TRUE) break;\r
206             else lits[ii] = lit;\r
207         }\r
208         if (tautologie == FALSE) {\r
209             sat[i]= (int *)malloc((length+1) * sizeof(int));\r
210             for (j=0; j<length; j++) {\r
211               if (lits[j] < 0) \r
212                   sat[i][j] = abs(lits[j]) - 1 + NB_VAR ;\r
213               else \r
214                   sat[i][j] = lits[j]-1;\r
215           }\r
216           sat[i][length]=NONE;\r
217           clause_length[i]=length;\r
218           clause_state[i] = ACTIVE;\r
219       }\r
220       else { i--; NB_CLAUSE--;}\r
221   }\r
222   return TRUE;\r
223 }\r
224 \r
225 void build_structure() {\r
226     int i, j, var, *lits1, length, clause, *vars_signs, lit;\r
227     for (i=0; i<NB_VAR; i++) { \r
228         neg_nb[i] = 0; pos_nb[i] = 0;\r
229     }\r
230     for (i=0; i<NB_CLAUSE; i++) {\r
231         for(j=0; j<clause_length[i]; j++) {\r
232             if (sat[i][j]>=NB_VAR) {\r
233                 var=sat[i][j]-NB_VAR; neg_nb[var]++;\r
234             }\r
235             else {\r
236                 var=sat[i][j]; \r
237                 pos_nb[var]++;\r
238             }\r
239         }\r
240         if (sat[i][clause_length[i]] !=NONE)\r
241             printf("erreur ");\r
242     }\r
243     for(clause=0;clause<NB_CLAUSE;clause++) {\r
244         length = clause_length[clause];\r
245         var_sign[clause] = (int *)malloc((2*length+1)*sizeof(int));\r
246         lits1 = sat[clause]; vars_signs = var_sign[clause];\r
247         for(lit=*lits1; lit!=NONE; lit=*(++lits1),(vars_signs+=2)) {\r
248             if (negative(lit)) {\r
249                 *(vars_signs+1)= NEGATIVE;\r
250                 *vars_signs = get_var_from_lit(lit);\r
251             }\r
252             else {\r
253                 *(vars_signs+1)=POSITIVE;\r
254                 *vars_signs = lit;\r
255             }\r
256         }\r
257         *vars_signs = NONE;  \r
258     }\r
259     for (i=0; i<NB_VAR; i++) { \r
260     neg_in[i] = (int *)malloc((neg_nb[i]+1) * sizeof(int));\r
261     pos_in[i] = (int *)malloc((pos_nb[i]+1) * sizeof(int));\r
262     neg_in[i][neg_nb[i]]=NONE; pos_in[i][pos_nb[i]]=NONE;\r
263     neg_nb[i] = 0; pos_nb[i] = 0;\r
264     var_state[i] = ACTIVE;\r
265   }   \r
266   for (i=0; i<NB_CLAUSE; i++) {\r
267     // if (i==774)\r
268     //  printf("kjhsdf");\r
269     lits1 = sat[i];\r
270     //printf("\n");\r
271     for(lit=*lits1; lit!=NONE; lit=*(++lits1)) {\r
272 \r
273       //  printf("   %d", get_var_from_lit(lit));\r
274         if (positive(lit)) \r
275             pos_in[lit][pos_nb[lit]++] = i;\r
276         else\r
277             neg_in[get_var_from_lit(lit)]\r
278                 [neg_nb[get_var_from_lit(lit)]++] = i;\r
279     }\r
280   }\r
281 }\r
282 \r
283 \r
284 void eliminate_redundance() {\r
285   int *lits, i, lit, *clauses, res, clause;\r
286 \r
287   for (i=0; i<NB_CLAUSE; i++) {\r
288     if (clause_state[i]==ACTIVE) {\r
289       if (clause_length[i]==1)\r
290         push(i, UNITCLAUSE_STACK);\r
291       lits = sat[i];\r
292       for(lit=*lits; lit!=NONE; lit=*(++lits)) {\r
293         if (positive(lit)) \r
294           clauses=pos_in[lit];\r
295         else clauses=neg_in[lit-NB_VAR];\r
296         for(clause=*clauses; clause!=NONE; clause=*(++clauses)) {\r
297           if ((clause<i) && (clause_state[clause]==ACTIVE)) {\r
298             res=redundant(sat[i], sat[clause]);\r
299             if (res==NEW_CLAUSE_REDUNDANT) {\r
300               clause_state[i]=PASSIVE;\r
301               break;\r
302             }\r
303             else if (res==OLD_CLAUSE_REDUNDANT)\r
304               clause_state[clause]=PASSIVE;\r
305           }\r
306         }\r
307         if (res==NEW_CLAUSE_REDUNDANT)\r
308           break;\r
309       }\r
310     }\r
311   }\r
312 }\r
313 \r
314 my_type build_simple_sat_instance(int vars_size,  const vector< vector<int> >&  clauses) {\r
315   \r
316     int i, j, length, NB_CLAUSE1, res, ii, jj, tautologie, lit1,\r
317         *pos_nb, *neg_nb;\r
318  \r
319     NB_VAR = vars_size;\r
320     NB_CLAUSE = clauses.size();\r
321 \r
322     INIT_NB_CLAUSE = NB_CLAUSE;\r
323     neg_nb=(int *)reduce_if_negative_nb;\r
324     pos_nb=(int *)reduce_if_positive_nb;\r
325 \r
326     if (lire_clauses(clauses)==FALSE)\r
327         return FALSE;\r
328     build_structure();\r
329     eliminate_redundance();\r
330     if (unitclause_process()==NONE) return NONE;\r
331     res=clean_structure();\r
332     if (res==FALSE)\r
333         return FALSE;\r
334     else if (res==SATISFIABLE)\r
335         return SATISFIABLE;\r
336     return TRUE;\r
337 }\r
338 \r
339 int verify_sol_input(char *input_file) {\r
340     FILE* fp_in=fopen(input_file, "r");\r
341   char ch, word2[WORD_LENGTH];\r
342   int i, j, lit, var, nb_var1, nb_clause1;\r
343 \r
344   if (fp_in == NULL) return FALSE;\r
345 \r
346   fscanf(fp_in, "%c", &ch);\r
347   while (ch!='p') {\r
348     while (ch!='\n') fscanf(fp_in, "%c", &ch);  \r
349     fscanf(fp_in, "%c", &ch);\r
350   }\r
351   \r
352   fscanf(fp_in, "%s%d%d", word2, &nb_var1, &nb_clause1);\r
353   for (i=0; i<nb_clause1; i++) {\r
354     fscanf(fp_in, "%d", &lit);\r
355     while (lit != 0) {\r
356       if (lit<0) {\r
357         if (var_current_value[abs(lit)-1]==FALSE)\r
358           break;\r
359       }\r
360       else {\r
361         if (var_current_value[lit-1]==TRUE)\r
362           break;\r
363       }\r
364       fscanf(fp_in, "%d", &lit);\r
365     }\r
366     if (lit==0) {\r
367       fclose(fp_in);\r
368       return FALSE;\r
369     }\r
370     else {\r
371       do fscanf(fp_in, "%d", &lit);\r
372       while (lit != 0) ;\r
373     }\r
374   }\r
375   fclose(fp_in);\r
376   return TRUE;\r
377 }\r