SLS求解器学习walkSAT3

  1 //cpick means computing break values and pick, this function is adopted for random 4-SAT
  2 int cpick_bbreak_gmake()
  3 {
  4     int        i,k,c,v,ci;
  5     int     bestvar_array[100];
  6     int        bestvar_count;
  7     int        best_bbreak;
  8     int        best_gmake;
  9     int        bbreakv,gmakev;
 10 
 11     int        *truep, *falsep;
 12     
 13     c = unsat_stack[rand()%unsat_stack_fill_pointer];
 14     
 15     //the first var
 16     v = clause_lit[c][0].var_num;
 17     truep = (cur_soln[v])? var_poslit[v]:var_neglit[v];
 18     
 19     bbreakv=0;
 20     for(; (ci=*truep)!=-1; ++truep)
 21     {
 22         if (sat_count[ci]==1) ++bbreakv;
 23     }
 24     
 25     best_bbreak = bbreakv;
 26     bestvar_array[0] = v;
 27     bestvar_count = 1;    
 28     
 29     //the remaining vars
 30     for(k=1; k<clause_lit_count[c]; ++k)
 31     {
 32         v = clause_lit[c][k].var_num;
 33         
 34         truep = (cur_soln[v])? var_poslit[v]:var_neglit[v];
 35         
 36         bbreakv=0;
 37         for(; (ci=*truep)!=-1; ++truep)
 38         {
 39             if (sat_count[ci]==1) 
 40             {
 41                 if (bbreakv == best_bbreak) break;
 42                 ++bbreakv;                    
 43             }
 44         }
 45         
 46         if(ci!=-1) continue;
 47         
 48         if (bbreakv < best_bbreak)
 49         {
 50             best_bbreak = bbreakv;
 51             bestvar_array[0] = v;
 52             bestvar_count = 1;
 53         }
 54         else// if (bbreakv == best_bbreak)
 55         {
 56             bestvar_array[bestvar_count]=v;
 57             ++bestvar_count;
 58         }
 59     }
 60 
 61     if(best_bbreak!=0 && (rand()%MY_RAND_MAX_INT)*BASIC_SCALE < wp) return clause_lit[c][rand()%clause_lit_count[c]].var_num;
 62 
 63     if(bestvar_count>1)
 64     {    
 65         int org_bestvar_count = bestvar_count;
 66         
 67         v = bestvar_array[0];
 68         
 69         falsep = cur_soln[v]?var_neglit[v]:var_poslit[v];
 70         
 71         gmakev=0;
 72         for(; (ci=*falsep)!=-1; ++falsep)
 73         {
 74             if (sat_count[ci]==1) gmakev+=b;
 75             else if (sat_count[ci]==0) gmakev+=a;
 76         }
 77         best_gmake = gmakev;
 78         //bestvar_array[0] = v;
 79         bestvar_count = 1;    
 80         
 81         for(i=1; i<org_bestvar_count; ++i)
 82         {
 83             v = bestvar_array[i];
 84             falsep = cur_soln[v]?var_neglit[v]:var_poslit[v];
 85             
 86             gmakev=0;
 87             for(; (ci=*falsep)!=-1; ++falsep)
 88             {
 89                 if (sat_count[ci]>1) continue;
 90                 if (sat_count[ci]==1) gmakev+=b; 
 91                 else //if (sat_count[ci]==0) 
 92                     gmakev+=a;
 93             }
 94             
 95             if (gmakev > best_gmake)
 96             {
 97                 best_gmake = gmakev;
 98                 bestvar_array[0] = v;
 99                 bestvar_count = 1;
100             }
101             else if (gmakev == best_gmake)
102             {
103                 bestvar_array[bestvar_count]=v;
104                 ++bestvar_count;
105             }
106         }
107     }
108     
109     return bestvar_array[rand()%bestvar_count];
110     
111     /*if(best_bbreak == 0) return bestvar_array[rand()%bestvar_count];
112 
113     if(rand()%MY_RAND_MAX_INT < scaledwp) return clause_lit[c][rand()%clause_lit_count[c]].var_num;
114     else    return bestvar_array[rand()%bestvar_count];*/
115     
116 }