# 学习阶段对蕴含图的复习

1.分析函数代码解读

 ``` 1 void Solver::analyze(CRef confl, vec& 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& ws = watches[p]; //文字p的观察watches[p]--是一个包含-p的观察元序列 23 Watcher *i, *j, *end; 24 num_props++; 25 26 vec& 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; i0) { 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 level_incs; level_incs.clear(); 65 for(int i=0; i1e100){ 77 for(int vv=0;vv

(0)
(0)

© 2014 mamicode.com 版权所有