标签：precise strong bsp dir cat lock 如何 put timer
一般来说学习子句lbd值的大小范围不同，认为其在今后发挥作用不同，lbd值越小，后续发挥作用越大，即认为其质量越高。依据lbd值的范围，在CDCL求器中有三个“木桶”供其存放。这三个集合分别是：
vec<CRef> learnts_core, learnts_tier2,learnts_local;
在求解过程中，学习子句进入、调整、删除等操作都是和这三个集合的定位紧密相关。
learnts_core —— 称为core学习子句集，其定位是进来的都是“高质量”学习子句，今后求解过程中遇到子句集规模管理时（相关reduced函数被调用时）不会被删除。
1.冲突分析中有三类学习子句进入learnts_core：
（1）调整原有子句进入core —— A。参与生成学习子句蕴含图上的个传播文字所对应的reason子句，见代码：confl = reason(var(p)); 按照现有的传播序列层次信息重新计算lbd值（调用函数lbd = computeLBD(c)），并依据条件判断进入core。见代码：
1 // Update LBD if improved. 2 if (c.learnt() && c.mark() != CORE){ 3 int lbd = computeLBD(c); 4 if (lbd < c.lbd()){ 5 if (c.lbd() <= 30) c.removable(false); // Protect once from reduction. 6 c.set_lbd(lbd); 7 if (lbd <= core_lbd_cut){ 8 learnts_core.push(confl); 9 c.mark(CORE); 10 }else if (lbd <= 6 && c.mark() == LOCAL){ 11 // Bug: ‘cr‘ may already be in ‘learnts_tier2‘, e.g., if ‘cr‘ was demoted from TIER2 12 // to LOCAL previously and if that ‘cr‘ is not cleaned from ‘learnts_tier2‘ yet. 13 learnts_tier2.push(confl); 14 c.mark(TIER2); } 15 } 16 17 if (c.mark() == TIER2) 18 c.touched() = conflicts; 19 else if (c.mark() == LOCAL) 20 claBumpActivity(c); 21 } 参与冲突生成的（在蕴含图中作为蕴含节点的）原属于iter2或local中的学习子句，此时有可能被调整到core集合中 |
（2）新生成的学习子句 —— 此时还是文字序列，被化简后输出为 vec<Lit>& out_learnt；会在search中依据lbd值确定是否进入core集合。
（3）化简函数中，依据现有传播序列层次信息更新lbd后调整，类似（1）。
针对学习子句集合的化简函数有多个：simplifyLearnt_tier2()、simplifyLearnt_core()、simplifyLearnt_x(vec<CRef>& learnts_x)，它们三个统一归simplifyAll()调用。
另有底层化简函数void Solver::simplifyLearnt(Clause& c)，是带参数的，针对对一个学习子句化简；它可以供以上学习子句集合函数调用。
2.进入core的学习子句的门槛：
（1）求解器给定的静态值core_lbd_cut；
（2）另一个门槛值是当冲突次数达到一个很大的值后，如果core集合中学习子句的数量很少，说明门槛太高，针对现有问题给定的core_lbd_cut太小了，于是主动降低门槛，将lbd门槛值做放大一些，但不能低于进入iter2的门槛lbd值。调整操作见函数search中的代码如下。
1 lbool Solver::search(int& nof_conflicts) 2 { 3 。。。 4 5 for (;;){ 6 propagationC = 0; //记录基于当前决策变量的传播数 // update on 2019-07-24 7 propagateLitC.clear(); // update on 2019-07-24 8 9 CRef confl = propagate(); 10 11 if (confl != CRef_Undef){ 12 // CONFLICT 13 if (VSIDS){ 14 if (--timer == 0 && var_decay < 0.95) timer = 5000, var_decay += 0.01; 15 }else 16 if (step_size > min_step_size) step_size -= step_size_dec; 17 18 conflicts++; nof_conflicts--; conflictC++; 19 propsize_queue.push(trail.size()); // Update on 2019-8-10 20 21 if (conflicts == 100000 && learnts_core.size() < 100) core_lbd_cut = 5; 22 ConflictData data = FindConflictLevel(confl); 23 if (data.nHighestLevel == 0) return l_False; 24 。。。25 }
|
learnts_tier2的定位是作为缓冲集合保存一些lbd适中的学习子句，考察他被最后使用时间刻度距离子句集整理时刻的远近，如太远表明很久没用，估计很大程度上今后也不会被使用，于是调整到local集合中。
1. 进入tier2的方式有三种：
与进入core的方式类同，（1）冲突分析时考察local更新过后的lbd值满足条件的进入；（2）学习子句新生成时依据lbd值判断条件进入iter2集合；（3）通用化简函数中调整，类同（1）。
2.关于tier2集合中学习子句调整：
（1）冲突分析中、化简中都会发生iter2向core输送更新lbd后符合条件的学习子句；也会发生local向iter2中输送更新lbd后符合条件的学习子句；
注意：有专门针对iter2集合的化简函数simplifyLearnt_core()，其中有专门的调整学习子句更新到core集合的代码。
1 bool Solver::simplifyLearnt_tier2() 2 { 3 int beforeSize, afterSize; 4 int learnts_tier2_size_before = learnts_tier2.size(); 5 6 int ci, cj, li, lj; 7 bool sat, false_lit; 8 unsigned int nblevels; 9 //// 10 //printf("learnts_x size : %d\n", learnts_x.size()); 11 12 //// 13 int nbSimplified = 0; 14 int nbSimplifing = 0; 15 16 for (ci = 0, cj = 0; ci < learnts_tier2.size(); ci++){ 17 CRef cr = learnts_tier2[ci]; 18 Clause& c = ca[cr]; 19 20 if (removed(cr)) continue; 21 else if (c.simplified()){ 22 learnts_tier2[cj++] = learnts_tier2[ci]; 23 //// 24 nbSimplified++; 25 } 26 else{ 27 int saved_size=c.size(); 28 // if (drup_file){ 29 // add_oc.clear(); 30 // for (int i = 0; i < c.size(); i++) add_oc.push(c[i]); } 31 //// 32 nbSimplifing++; 33 sat = false_lit = false; 34 for (int i = 0; i < c.size(); i++){ 35 if (value(c[i]) == l_True){ 36 sat = true; 37 break; 38 } 39 else if (value(c[i]) == l_False){ 40 false_lit = true; 41 } 42 } 43 if (sat){ 44 removeClause(cr); 45 } 46 else{ 47 detachClause(cr, true); 48 49 if (false_lit){ 50 for (li = lj = 0; li < c.size(); li++){ 51 if (value(c[li]) != l_False){ 52 c[lj++] = c[li]; 53 } 54 } 55 c.shrink(li - lj); 56 } 57 58 beforeSize = c.size(); 59 assert(c.size() > 1); 60 // simplify a learnt clause c 61 simplifyLearnt(c); 62 assert(c.size() > 0); 63 afterSize = c.size(); 64 65 if(drup_file && saved_size!=c.size()){ 66 67 #ifdef BIN_DRUP 68 binDRUP(‘a‘, c , drup_file); 69 // binDRUP(‘d‘, add_oc, drup_file); 70 #else 71 for (int i = 0; i < c.size(); i++) 72 fprintf(drup_file, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1)); 73 fprintf(drup_file, "0\n"); 74 75 // fprintf(drup_file, "d "); 76 // for (int i = 0; i < add_oc.size(); i++) 77 // fprintf(drup_file, "%i ", (var(add_oc[i]) + 1) * (-2 * sign(add_oc[i]) + 1)); 78 // fprintf(drup_file, "0\n"); 79 #endif 80 } 81 82 //printf("beforeSize: %2d, afterSize: %2d\n", beforeSize, afterSize); 83 84 if (c.size() == 1){ 85 // when unit clause occur, enqueue and propagate 86 uncheckedEnqueue(c[0]); 87 if (propagate() != CRef_Undef){ 88 ok = false; 89 return false; 90 } 91 // delete the clause memory in logic 92 c.mark(1); 93 ca.free(cr); 94 //#ifdef BIN_DRUP 95 // binDRUP(‘d‘, c, drup_file); 96 //#else 97 // fprintf(drup_file, "d "); 98 // for (int i = 0; i < c.size(); i++) 99 // fprintf(drup_file, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1)); 100 // fprintf(drup_file, "0\n"); 101 //#endif 102 } 103 else{ 104 attachClause(cr); 105 learnts_tier2[cj++] = learnts_tier2[ci]; 106 107 nblevels = computeLBD(c); 108 if (nblevels < c.lbd()){ 109 //printf("lbd-before: %d, lbd-after: %d\n", c.lbd(), nblevels); 110 c.set_lbd(nblevels); 111 } 112 113 if (c.lbd() <= core_lbd_cut){ 114 cj--; 115 learnts_core.push(cr); 116 c.mark(CORE); 117 } 118 119 c.setSimplified(true); 120 } 121 } 122 } 123 } 124 learnts_tier2.shrink(ci - cj); 125 126 // printf("c nbLearnts_tier2 %d / %d, nbSimplified: %d, nbSimplifing: %d\n", 127 // learnts_tier2_size_before, learnts_tier2.size(), nbSimplified, nbSimplifing); 128 129 return true; 130 131 }
|
（2）iter2中的学习子句调整到local集合是调整的主流方向。
1 void Solver::reduceDB_Tier2() 2 { 3 int i, j; 4 for (i = j = 0; i < learnts_tier2.size(); i++){ 5 Clause& c = ca[learnts_tier2[i]]; 6 if (c.mark() == TIER2) 7 if (!locked(c) && c.touched() + 30000 < conflicts){ 8 learnts_local.push(learnts_tier2[i]); 9 c.mark(LOCAL); 10 //c.removable(true); 11 c.activity() = 0; 12 claBumpActivity(c); 13 }else 14 learnts_tier2[j++] = learnts_tier2[i]; 15 } 16 learnts_tier2.shrink(i - j); 17 } 我们看到，iter2考察的主要是c.touched()，也就是该学习子句最后一次使用的时间刻度（用求解进展中所处的求解器冲突计数时钟值标定） |
learnts_local学习子句集
1.进出local集合的途径上面已经提到。（1）在冲突分析函数、化简函数中符合条件转出到core或iter2；（2）search函数中冲突分析最终新生的学习子句符合条件进入；（3）专门函数reduceDB_Tier2()从iter2中批量转入；
2.对学习子句删除都是针对local学习子句集。
（1）reduceDB()函数代码如下：（最简单的版本）
1 void Solver::reduceDB() 2 { 3 int i, j; 4 //if (local_learnts_dirty) cleanLearnts(learnts_local, LOCAL); 5 //local_learnts_dirty = false; 6 7 sort(learnts_local, reduceDB_lt(ca)); 8 9 int limit = learnts_local.size() / 2; 10 11 for (i = j = 0; i < learnts_local.size(); i++) 12 { 13 Clause& c = ca[learnts_local[i]]; 14 15 if (c.mark() == LOCAL) 16 { 17 if ( c.removable() && !locked(c) && i < limit) 18 removeClause(learnts_local[i]); 19 else 20 { 21 if (!c.removable()) limit++; 22 c.removable(true); 23 learnts_local[j++] = learnts_local[i]; 24 } 25 } 26 } 27 learnts_local.shrink(i - j); 28 checkGarbage(); 29 } 子句管理涉及三个问题：（1）什么时候删除？（2）删除多少？（3）删除那些？ 针对这三个问题管理local学习几句的规模。以后很多文献做这方面的研究。我此时思考：学习子句的管理和求解器重启两个模块启动的时间点目前是不同步的，这是有特殊考虑吗？不同步的程度如何刻画出来？是否和其它信息相关？ |
（2）针对local的管理是基于学习子句活跃度排序的。涉及两个问题：排序依据子句活跃度是在那些地方计算得到的？如何排序？
如何排序，学习子句集中存储的是CRef类型的子句指针，需要设计专门的数据结构，供sort排序函数调用。
1 struct VarOrderLt { 2 const vec<double>& activity; 3 bool operator () (Var x, Var y) const { return activity[x] > activity[y]; } 4 VarOrderLt(const vec<double>& act) : activity(act) { } 5 }; 为了变元活跃度的排序，Solver.h文件中定义的结构体类型VarOrderLt，重载operator ()定义了比较关系。类似以上代码，Solver.cc文件中在函数reduceDB()前定义了下面的结构体类型： |
1 struct reduceDB_lt { 2 ClauseAllocator& ca; 3 reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {} 4 bool operator () (CRef x, CRef y) const { return ca[x].activity() < ca[y].activity(); } 5 }; 并使用了下面的函数进行学习子句活跃度的排序： 1 sort(learnts_local, reduceDB_lt(ca));
该函数是在模板函数及算法文件夹mtl内Sort.h文件中定义的。sort函数有多个重载，我们这里直接用到的带两个参数的函数，其中调用了带三个参数的函数。 1 template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) { 2 sort((T*)v, v.size(), lt); }
1 template <class T, class LessThan> 2 void sort(T* array, int size, LessThan lt) 3 { 4 if (size <= 15) 5 selectionSort(array, size, lt); 6 7 else{ 8 T pivot = array[size / 2]; 9 T tmp; 10 int i = -1; 11 int j = size; 12 13 for(;;){ 14 do i++; while(lt(array[i], pivot)); 15 do j--; while(lt(pivot, array[j])); 16 17 if (i >= j) break; 18 19 tmp = array[i]; array[i] = array[j]; array[j] = tmp; 20 } 21 22 sort(array , i , lt); 23 sort(&array[i], size-i, lt); 24 } 25 } 其中第5行，如果需要排序的量过小，采用选择排序方法，量较大时，采用了折半查找排序的优化代码。 其中用到的选择排序函数以及相关定义如下： 1 template<class T> 2 struct LessThan_default { 3 bool operator () (T x, T y) { return x < y; } 4 }; 5 6 7 template <class T, class LessThan> 8 void selectionSort(T* array, int size, LessThan lt) 9 { 10 int i, j, best_i; 11 T tmp; 12 13 for (i = 0; i < size-1; i++){ 14 best_i = i; 15 for (j = i+1; j < size; j++){ 16 if (lt(array[j], array[best_i])) 17 best_i = j; 18 } 19 tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; 20 } 21 } 22 template <class T> static inline void selectionSort(T* array, int size) { 23 selectionSort(array, size, LessThan_default<T>()); }
|
（3）真正的释放删除学习子句后的存储空间，是在函数checkGarbage()之中完成的。
1 void Solver::removeClause(CRef cr) { 2 Clause& c = ca[cr]; 3 4 if (drup_file){ 5 if (c.mark() != 1){ 6 #ifdef BIN_DRUP 7 binDRUP(‘d‘, c, drup_file); 8 #else 9 fprintf(drup_file, "d "); 10 for (int i = 0; i < c.size(); i++) 11 fprintf(drup_file, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1)); 12 fprintf(drup_file, "0\n"); 13 #endif 14 }else 15 printf("c Bug. I don‘t expect this to happen.\n"); 16 } 17 18 detachClause(cr); 19 // Don‘t leave pointers to free‘d memory! 20 if (locked(c)){ 21 Lit implied = c.size() != 2 ? c[0] : (value(c[0]) == l_True ? c[0] : c[1]); 22 vardata[var(implied)].reason = CRef_Undef; } 23 c.mark(1); 24 25 ca.free(cr); 26 } 以上删除学习子句的方式与化简函数中，都使用 ca.free(cr)。 |
（4）我们注意到local管理删除一众学习子句之后，函数的最后两行代码是：
learnts_local.shrink(i - j); //向量收缩，释放一些空间
checkGarbage(); //管理内存空间。由代码可以看出，它并不是马上缩小所向操作系统争取到的空，而是估计现有空间利用度之后再做决定是否释放。
1 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); } 2 inline void Solver::checkGarbage(double gf){ 3 if (ca.wasted() > ca.size() * gf) 4 garbageCollect(); } |
1 void Solver::garbageCollect() 2 { 3 // Initialize the next region to a size corresponding to the estimated utilization degree. This 4 // is not precise but should avoid some unnecessary reallocations for the new region: 5 ClauseAllocator to(ca.size() - ca.wasted()); 6 7 relocAll(to); 8 if (verbosity >= 2) 9 printf("c | Garbage collection: %12d bytes => %12d bytes |\n", 10 ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); 11 to.moveTo(ca); 12 }
|
| 以上删除学习子句的方式与化简函数中，都使用的 ca.free(cr)。 |
标签：precise strong bsp dir cat lock 如何 put timer
原文地址：https://www.cnblogs.com/yuweng1689/p/13061584.html
