analyze和collectFirstUIP函数都非常巧妙地使用pathCs和seen进行遍历冲突生成的传播路径
注意：相关修改和借用，需要确保reason中的c0为BCP蕴含文字。
由于传播函数在处理观察时未对watches_bin的观察元对应子句做相应的文字调整处理，所以最为直接的方法是在传播阶段确保二元子句作为reason时蕴含文字处在0位置，对下面两个函数增加部分代码：
1 void Solver::uncheckedEnqueue(Lit p, CRef from) 2 { 3 assert(value(p) == l_Undef); 4 //==================================================== 5 if (from != CRef_Undef) { 6 Clause& c = ca[from]; 7 if (p != lit_Undef && c.size() == 2 && c[0] != p) { 8 assert(value(c[0]) == l_False); 9 assert(c[1] == p); 10 Lit tmp = c[0]; 11 c[0] = c[1], c[1] = tmp; 12 } 13 } 14 //==================================================== 15 16 Var x = var(p); 17 if (!VSIDS){ 18 picked[x] = conflicts; 19 conflicted[x] = 0; 20 almost_conflicted[x] = 0; 21 #ifdef ANTI_EXPLORATION 22 uint32_t age = conflicts - canceled[var(p)]; 23 if (age > 0){ 24 double decay = pow(0.95, age); 25 activity_CHB[var(p)] *= decay; 26 if (order_heap_CHB.inHeap(var(p))) 27 order_heap_CHB.increase(var(p)); 28 } 29 #endif 30 } 31 32 assigns[x] = lbool(!sign(p)); 33 vardata[x] = mkVarData(from, decisionLevel()); 34 trail.push_(p); 35 }
|
|
1 void Solver::simpleUncheckEnqueue(Lit p, CRef from){ 2 assert(value(p) == l_Undef); 3 //=================================================== 4 if (from != CRef_Undef) { 5 Clause& c = ca[from]; 6 if (p != lit_Undef && c.size() == 2 && c[0] != p) { 7 assert(value(c[0]) == l_False); 8 assert(c[1] == p); 9 Lit tmp = c[0]; 10 c[0] = c[1], c[1] = tmp; 11 } 12 } 13 //=================================================== 14 assigns[var(p)] = lbool(!sign(p)); // this makes a lbool object whose value is sign(p) 15 vardata[var(p)].reason = from; 16 trail.push_(p); 17 }
|
|