学习阶段对蕴含图的复习

  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 /*_________________________________________________________________________________________________
  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 }

 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 }