SLS求解器学习walkSAT3

Posted 2021-03-03 yuweng1689

walksat2013版本的函数

 

重点函数之一

  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 }

 

我自己敲一遍顺便做些注释。如下：

int cpick_bbreak_gmake()

{

    int    i,k,c,v,ci;　　　　　　　　// c通常代表子句编号； v通常代表变元； ci通常代表子句中的元素（文字）

    int   bestvar_array[100];

    int  bestvar_count;

    int  best_bbreak;

    int  best_gmake;

    int  bbreakv, gmakev;

    int *truep,  *falsep;　　　　　　//这两个指针的移动可以用来指示子句序列——这些子句包含特定变元（分为两类，分别是以正、负文字形式出现在子句中的）。

    //-----------------------------------------

    c = unsat_stack[rand()%unsat_stack_fill_pointer];  //从栈中任选一个子句；unsat_satck_fill_pointer是栈内元素的个数，该值也作为栈顶的指示变量

    v = clause_lit[c][0].var_num;　　//选择子句clause_lit[c]的0号位置上的文字，取它的变元。

    truep = ( cur_soln[v] ) ? var_poslit[v] : var_neglit[v]; //变元v赋值为1/0，分别取v以正/负文字出现的子句序列头指针（数组名）赋给truep（这样他总数获得v以为真的形式出现的头指针）。

    bbreakv = 0;

    for (;(ci = *truep) != -1; ++truep)

    {

        if (sat_cout[ci] == 1)  bbreakv++;    //bbreakv 记录c子句0号文字变元所对应的为真出现的全体子句中，有一个真文字的子句个数。

                                                               //即得到v所关联的sat子句个数（v在子句中为唯一真文字）。翻转该文字能将该子句从sat变为unsat。

    }