学习阶段对蕴含图的复习

技术文章 7个月前 完美者
1,195 0

标签:sse   locker   elb   int   push   gen   previous   height   函数   

1.分析函数代码解读

 
  1 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, int& out_lbd)
  2 {
  3     int pathC = 0;         //从冲突子句回溯路径上的分叉数
  4     Lit p     = lit_Undef; //p最终是冲突文字(相冲突的两个子句中互为补文字,其中一个已经传播保存在trail之中,另一个记录在confl中的confl[0])
  5 
  6     // Generate conflict clause:
  7     //
  8     out_learnt.push();      // (leave room for the asserting literal)
  9     int index   = trail.size() - 1;
 10     int nDecisionLevel = level(var(ca[confl][0]));  //保存在trail的冲突文字可能在冲突支配文字之前(同层或之前的层),也可能在之后(同层);
 11     assert(nDecisionLevel == level(var(ca[confl][0])));
 12 
 13     do{
 14         assert(confl != CRef_Undef); // (otherwise should be UIP)
 15         Clause& c = ca[confl];  //从冲突点冲突子句发起对蕴含图的回溯
 16         /////////////////////////////////////////////////////////////////////////mark no. used
 17         if (c.learnt() && c.usedt()<200)
 18         {
 19             c.set_usedt(c.usedt()+1); 
 20         }
 21         /////////////////////////////////////////////////////////////////////////
 22 
 23         // For binary clauses, we don‘t rearrange literals in propagate(), so check and make sure the first is an implied lit.
 24         if (p != lit_Undef && c.size() == 2 && value(c[0]) == l_False){
 25             assert(value(c[1]) == l_True);
 26             Lit tmp = c[0];
 27             c[0] = c[1], c[1] = tmp; }  //是对propagate函数的补位,二值观察元0/1直至只有一个为真,此处确保c[0]为真,即c[0]为蕴含的文字
 28 
 29         // Update LBD if improved.
 30         if (c.learnt() && c.mark() != CORE){
 31             int lbd = computeLBD(c);
 32             if (lbd < c.lbd()){
 33                 if (c.lbd() <= 30) c.removable(false); // Protect once from reduction.
 34                 c.set_lbd(lbd);
 35                 if (lbd <= core_lbd_cut){
 36                     learnts_core.push(confl);
 37                     c.mark(CORE);
 38                 }else if (lbd <= 6 && c.mark() == LOCAL){
 39                     // Bug: ‘cr‘ may already be in ‘learnts_tier2‘, e.g., if ‘cr‘ was demoted from TIER2
 40                     // to LOCAL previously and if that ‘cr‘ is not cleaned from ‘learnts_tier2‘ yet.
 41                     learnts_tier2.push(confl);
 42                     c.mark(TIER2); }
 43             }
 44 
 45             if (c.mark() == TIER2)
 46                 c.touched() = conflicts;
 47             else if (c.mark() == LOCAL)
 48                 claBumpActivity(c);
 49         }
 50 
 51         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
 52             Lit q = c[j];
 53 
 54             if (!seen[var(q)] && level(var(q)) > 0){
 55                 if (VSIDS){
 56                     varBumpActivity(var(q), .5);
 57                     add_tmp.push(q);
 58                 }else
 59                     conflicted[var(q)]++;
 60                 seen[var(q)] = 1;
 61                 if (level(var(q)) >= nDecisionLevel){
 62                     pathC++;
 63                 }else
 64                     out_learnt.push(q);
 65             }
 66         }
 67         
 68         // Select next clause to look at:
 69         do {
 70             while (!seen[var(trail[index--])]);  //此处函数体为空语句(只有分号),在trail上移动index从后往前找到一个分叉口(蕴含图节点)
 71             p  = trail[index+1];
 72         } while (level(var(p)) < nDecisionLevel);
 73         
 74         confl = reason(var(p)); //蕴含节点转移到边上(该指向该节点的若干条边为同一个蕴含子句)
 75         seen[var(p)] = 0;  //该节点完成使命——查找到蕴含子句,得到多个该节点向后回溯能够到达的节点(在该蕴含子句confl之中)
 76         pathC--;
 77 
 78     }while (pathC > 0);       //此do-while类似工作栈将冲突点之后的“参与冲突的子句和节点”深度搜索一遍;
//同时蕴含图完成切割,切割线由在trail中的冲突文字的所在层数决定,见line10,
//设定标准见line61-64,大于等于nDecisionLevel继续回溯,小于的不在回溯了。
79 out_learnt[0] = ~p; //唯一蕴含点p找到了(唯一蕴含点可能是冲突层决策变元,也可能是),取反放入学习子句0位置。 80 81 // Simplify conflict clause: 82 // 83 int i, j; 84 out_learnt.copyTo(analyze_toclear); //此时学习子句out_learnt中文字的可见性没有都为0,在line158中一并处理为0. 85 if (ccmin_mode == 2){ 86 uint32_t abstract_level = 0; 87 for (i = 1; i < out_learnt.size(); i++) 88 abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) 89 90 for (i = j = 1; i < out_learnt.size(); i++) 91 if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level)) 92 out_learnt[j++] = out_learnt[i]; 93 94 }else if (ccmin_mode == 1){ 95 for (i = j = 1; i < out_learnt.size(); i++){ 96 Var x = var(out_learnt[i]); 97 98 if (reason(x) == CRef_Undef) 99 out_learnt[j++] = out_learnt[i]; 100 else{ 101 Clause& c = ca[reason(var(out_learnt[i]))]; 102 for (int k = c.size() == 2 ? 0 : 1; k < c.size(); k++) 103 if (!seen[var(c[k])] && level(var(c[k])) > 0){ 104 out_learnt[j++] = out_learnt[i]; 105 break; } 106 } 107 } 108 }else 109 i = j = out_learnt.size(); 110 111 max_literals += out_learnt.size(); 112 out_learnt.shrink(i - j); 113 tot_literals += out_learnt.size(); 114 115 out_lbd = computeLBD(out_learnt); 116 if (out_lbd <= 6 && out_learnt.size() <= 30) // Try further minimization? 117 if (binResMinimize(out_learnt)) 118 out_lbd = computeLBD(out_learnt); // Recompute LBD if minimized. 119 120 // Find correct backtrack level: 121 // 122 if (out_learnt.size() == 1) 123 out_btlevel = 0; 124 else{ 125 int max_i = 1; 126 // Find the first literal assigned at the next-highest level: 127 for (int i = 2; i < out_learnt.size(); i++) 128 if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) 129 max_i = i; 130 // Swap-in this literal at index 1: 131 Lit p = out_learnt[max_i]; 132 out_learnt[max_i] = out_learnt[1]; 133 out_learnt[1] = p; 134 out_btlevel = level(var(p)); 135 } 136 137 if (VSIDS){ 138 for (int i = 0; i < add_tmp.size(); i++){ 139 Var v = var(add_tmp[i]); 140 if (level(v) >= out_btlevel - 1) 141 varBumpActivity(v, 1); 142 } 143 add_tmp.clear(); 144 }else{ 145 seen[var(p)] = true; 146 for(int i = out_learnt.size() - 1; i >= 0; i--){ 147 Var v = var(out_learnt[i]); 148 CRef rea = reason(v); 149 if (rea != CRef_Undef){ 150 const Clause& reaC = ca[rea]; 151 for (int i = 0; i < reaC.size(); i++){ 152 Lit l = reaC[i]; 153 if (!seen[var(l)]){ 154 seen[var(l)] = true; 155 almost_conflicted[var(l)]++; 156 analyze_toclear.push(l); } } } } } 157 158 for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // (‘seen[]‘ is now cleared) 159 }

 

 

阅读笔记:

   1.    seen[v]是个用来替代工作栈进行回溯查找的好工具。与trail配合可以回溯查找唯一蕴含点并完成切割。

   2.   almost_conflicted[v]记录每一个变元参与

 

 

2.传播函数propagate代码解读

 
  1 /*_________________________________________________________________________________________________
  2 |
  3 |  propagate : [void]  ->  [Clause*]
  4 |  
  5 |  Description:
  6 |    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
  7 |    otherwise CRef_Undef.
  8 |  
  9 |    Post-conditions:
 10 |      * the propagation queue is empty, even if there was a conflict.
 11 |________________________________________________________________________________________________@*/
 12 CRef Solver::propagate()
 13 {
 14     CRef    confl     = CRef_Undef;
 15     int     num_props = 0;
 16     watches.cleanAll();
 17     watches_bin.cleanAll();                      //观察体系进行除重操作
 18     //printf("find pro 001\n");
 19     while (qhead < trail.size()){
 20         Lit            p   = trail[qhead++];     // ‘p‘ is enqueued fact to propagate.
 21         int currLevel = level(var(p));           
 22         vec<Watcher>&  ws  = watches[p];         //文字p的观察watches[p]--是一个包含-p的观察元序列
 23         Watcher        *i, *j, *end;
 24         num_props++;
 25 
 26         vec<Watcher>& ws_bin = watches_bin[p];  // Propagate binary clauses first.
 27         for (int k = 0; k < ws_bin.size(); k++){
 28             Lit the_other = ws_bin[k].blocker;
 29             if (value(the_other) == l_False){
 30                 confl = ws_bin[k].cref;
 31 #ifdef LOOSE_PROP_STAT
 32                 return confl;
 33 #else
 34                 goto ExitProp;
 35 #endif
 36             }else if(value(the_other) == l_Undef)
 37             {
 38                 uncheckedEnqueue(the_other, currLevel, ws_bin[k].cref);
 39 #ifdef  PRINT_OUT                
 40                 std::cout << "i " << the_other << " l " << currLevel << "\n";
 41 #endif                
 42             }
 43         }
 44 
 45         for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
 46             // Try to avoid inspecting the clause:
 47             Lit blocker = i->blocker;
 48             if (value(blocker) == l_True){
 49                 *j++ = *i++; continue; }
 50 
 51             // Make sure the false literal is data[1]:
 52             CRef     cr        = i->cref;
 53             Clause&  c         = ca[cr];
 54             Lit      false_lit = ~p;
 55             if (c[0] == false_lit)
 56                 c[0] = c[1], c[1] = false_lit;  //二值观察数据结构观察子句的前两个文字。此处确保c[1]文字是假,c[0]才有可能是蕴含出的文字
 57                                                 //c[1]为-p,那么c[0]有通常是观察watcher[p]中观察元的bolcker
 58             assert(c[1] == false_lit);
 59             i++;
 60 
 61             // If 0th watch is true, then clause is already satisfied.
 62             Lit     first = c[0];    //c子句中的文字顺利可以被调整(见行1616),再经行1602~1603调整c[0]有可能不是原来bolcker
 63             Watcher w     = Watcher(cr, first); //准备一个观察元--正在被排查的子句为cref,first为blocker。
 64             if (first != blocker && value(first) == l_True){  //first 
 65                 *j++ = w; continue; }           //替换当前观察watcher[p]中当前观察元为新观察元
 66             //以上被排查子句已经有为真的文字则continue
 67 
 68             //如果被排查的子句准备被蕴含的文字不为真,则剩余可能有两种:为l_False或l_Undef
 69             // Look for new watch:
 70             for (int k = 2; k < c.size(); k++)
 71                 if (value(c[k]) != l_False){
 72                     c[1] = c[k]; c[k] = false_lit;  //已经为假的文字后移
 73                     watches[~c[1]].push(w);         //为其它观察补充观察元        
 74                     goto NextClause; }
 75 
 76             // Did not find watch -- clause is unit under assignment:
 77             *j++ = w;
 78             if (value(first) == l_False){   //剩余可能有两种之一:为l_False
 79                 confl = cr;
 80                 qhead = trail.size();
 81                 // Copy the remaining watches:
 82                 while (i < end)
 83                     *j++ = *i++;
 84             }else                          //剩余可能有两种之二:为l_Undef
 85             {
 86                 if (currLevel == decisionLevel())
 87                 {
 88                     uncheckedEnqueue(first, currLevel, cr);
 89 #ifdef PRINT_OUT                    
 90                     std::cout << "i " << first << " l " << currLevel << "\n";
 91 #endif                    
 92                 }
 93                 else
 94                 {
 95                     int nMaxLevel = currLevel;
 96                     int nMaxInd = 1;
 97                     // pass over all the literals in the clause and find the one with the biggest level
 98                     for (int nInd = 2; nInd < c.size(); ++nInd)
 99                     {
100                         int nLevel = level(var(c[nInd]));
101                         if (nLevel > nMaxLevel)
102                         {
103                             nMaxLevel = nLevel;
104                             nMaxInd = nInd;
105                         }
106                     }
107 
108                     if (nMaxInd != 1)
109                     {
110                         std::swap(c[1], c[nMaxInd]);
111                         *j--; // undo last watch
112                         watches[~c[1]].push(w);
113                     }
114                     
115                     uncheckedEnqueue(first, nMaxLevel, cr);
116 #ifdef PRINT_OUT                    
117                     std::cout << "i " << first << " l " << nMaxLevel << "\n";
118 #endif    
119                 }
120             }
121 
122 NextClause:;
123         }
124         ws.shrink(i - j);
125     }
126 
127     //printf("find pro 002\n");
128 
129 ExitProp:;
130     propagations += num_props;
131     simpDB_props -= num_props;
132 
133     return confl;
134 }

 

   

 

3.记录参与冲突生成的蕴含图节点及举例冲突点距离的函数--距离越远说明越早参与传播(在trail中靠前),对冲突形成越重要

 
 1 // pathCs[k] is the number of variables assigned at level k,
 2 // it is initialized to 0 at the begining and reset to 0 after the function execution
 3 bool Solver::collectFirstUIP(CRef confl){
 4     involved_lits.clear();
 5     int max_level = 1;
 6     Clause& c = ca[confl]; int minLevel = decisionLevel();
 7     for(int i = 0; i<c.size(); i++) {
 8         Var v = var(c[i]);
 9         //        assert(!seen[v]);
10         if (level(v)>0) {
11             seen[v]=1;
12             var_iLevel_tmp[v] = 1;
13             pathCs[level(v)]++;
14             if (minLevel > level(v)) {
15                 minLevel = level(v);
16                 assert(minLevel>0);
17             }
18             //    varBumpActivity(v);
19         }
20     }
21 
22     int limit = trail_lim[minLevel-1];
23     for(int i = trail.size()-1; i>=limit; i--) {
24         Lit p = trail[i]; Var v = var(p);
25         if (seen[v]) {
26             int currentDecLevel = level(v);
27             //      if (currentDecLevel == decisionLevel())
28             //          varBumpActivity(v);
29             seen[v] = 0;
30             if (--pathCs[currentDecLevel]!=0) {
31                 Clause& rc=ca[reason(v)];
32                 int reasonVarLevel=var_iLevel_tmp[v]+1;
33                 if(reasonVarLevel>max_level) max_level=reasonVarLevel;
34                 if (rc.size() == 2 && value(rc[0]) == l_False) {
35                     // Special case for binary clauses
36                     // The first one has to be SAT
37                     assert(value(rc[1]) != l_False);
38                     Lit tmp = rc[0];
39                     rc[0] =  rc[1], rc[1] = tmp;
40                 }
41                 for (int j = 1; j < rc.size(); j++){
42                     Lit q = rc[j]; Var v1 = var(q);
43                     if (level(v1) > 0) {
44                         if (minLevel>level(v1)) {
45                             minLevel = level(v1); limit = trail_lim[minLevel-1];     assert(minLevel>0);
46                         }
47                         if (seen[v1]) {
48                             if (var_iLevel_tmp[v1] < reasonVarLevel)
49                                 var_iLevel_tmp[v1] = reasonVarLevel;
50                         }
51                         else {
52                             var_iLevel_tmp[v1] = reasonVarLevel;
53                             //   varBumpActivity(v1);
54                             seen[v1] = 1;
55                             pathCs[level(v1)]++;
56                         }
57                     }
58                 }
59             }
60             involved_lits.push(p);
61         }
62     }
63     double inc = var_iLevel_inc;
64     vec<int> level_incs; level_incs.clear();
65     for(int i=0; i<max_level; i++){
66         level_incs.push(inc);
67         inc = inc/my_var_decay;
68     }
69 
70     for(int i=0; i<involved_lits.size(); i++){
71         Var v =var(involved_lits[i]);
72         //        double old_act = activity_distance[v];
73         //        activity_distance[v] += var_iLevel_inc * var_iLevel_tmp[v];
74         activity_distance[v] += var_iLevel_tmp[v]*level_incs[var_iLevel_tmp[v]-1];
75 
76         if(activity_distance[v]>1e100){
77             for(int vv=0;vv<nVars();vv++)
78                 activity_distance[vv] *= 1e-100;
79             var_iLevel_inc*=1e-100;
80             for(int j=0; j<max_level; j++) level_incs[j]*=1e-100;
81         }
82         if (order_heap_distance.inHeap(v))
83             order_heap_distance.decrease(v);
84 
85         //        var_iLevel_inc *= (1 / my_var_decay);
86     }
87     var_iLevel_inc = level_incs[level_incs.size()-1];
88     return true;
89 }

 

   

 

学习阶段对蕴含图的复习

标签:sse   locker   elb   int   push   gen   previous   height   函数   

原文地址:https://www.cnblogs.com/yuweng1689/p/14235125.html

版权声明:完美者 发表于 2021-01-07 12:44:07。
转载请注明:学习阶段对蕴含图的复习 | 完美导航

暂无评论

暂无评论...