变元的相位活跃度初始化方法

Posted 2021-03-02 yuweng1689

第一种方法：直接采用随机赋值的方法

---

 1.在初始时任意指派（真l_True 或者 假l_False）

 

 

 2.回溯阶段采用技术，保留原来相位，相位转换交给回溯层变元翻转。

 1 // Revert to the state at given level (keeping all assignment at ‘level‘ but not beyond).
 2 //
 3 void Solver::cancelUntil(int clevel) {
 4     if (decisionLevel() > clevel){
 5         for (int c = trail.size()-1; c >= trail_lim[clevel]; c--){
 6             Var      x  = var(trail[c]);
 7 
 8             if (!VSIDS){ //CHB:conflict history based
 9                 uint32_t age = conflicts - decisionTime[x];
10                 if (age >0){
11                     double adjusted_reward =  varBumpCnt[x]/(double) age;
12                     double old_activity = activity[x];
13                     activity[x] = alpha * adjusted_reward + ( beta * old_activity);
14                     if (order_heap.inHeap(x)){
15                         if (activity[x] > old_activity) order_heap.decrease(x);
16                         else order_heap.increase(x);
17                     }
18                 }
19                 canceled[x] = conflicts;
20             }
21 
22             assigns [x] = l_Undef;
23             if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
24                 polarity[x] = sign(trail[c]);
25             insertVarOrder(x); }
26         qhead = trail_lim[clevel];
27         trail.shrink(trail.size() - trail_lim[clevel]);
28         trail_lim.shrink(trail_lim.size() - clevel);
29     } 
30 }

 

 

 

第二种方法：依据cnf公式原始结构信息（详细信息可见：）

---

 1 lbool Solver::solve_()
 2 {
 3      ...
 4      if(solves==0){
 5         vec<double> occs;
 6         occs.growTo(2*nVars(),0.0);
 7         for(int i=0; i<nClauses(); ++i){
 8             const Clause &c = ca[clauses[i]];
 9             double increment = 1/(double)(c.size()*c.size());
10             for(int j=0; j<c.size(); ++j){
11                 occs[toInt(c[j])]=occs[toInt(c[j])]+increment;
12             }
13         }
14         for(int i=0; i<nVars(); ++i){
15             polarity[i]=occs[2*i]<=occs[2*i+1]; // initial polarity is false if the positive lit occurs more than the negative in the theory.
16             activity[i]=occs[2*i]*occs[2*i+1];
17         }
18         rebuildOrderHeap();
19     }
20 
21      ...
22 }

 参考文献：

The initial phase of a decision variable in
this solver is similar to the solver inIDGlucose [10]. That is,
it is set by weighting a literal occurrence in the original CNF.

[10] Devriendt J.: inIDGlucose, Proceedings of SAT Competition 2018, p.41

 

 

 

第三种方法：PSIDS ------ Polarity State Independent Decaying Sum heuristic.

---

 

    We keep for each variable in the solver two scores for its positive and negative polarities respectively.

    Each time a polarity — of a variable — is set in the solver, the activity of the latter is increased, and when a decision is made using the branching heuristic, then the most active polarity is chosen.

    As with VSIDS, we decrease from time to time the activities of all polarities (of all variables) in order to favor most recent ones.

    代码可以参见2019年求解器：PSIDS_MapleLCMDistChronoBT