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 }
|
|
标签：Undef,collectFirstUIP,pathCs,value,assert,&&,var,seen,CRef From： https://www.cnblogs.com/yuweng1689/p/17713426.html