一些重要笔记整理
1.变元v的decision[v部分变元不参与活跃度排序
在读入cnf文件时，首先调用的是newVars函数，该函数调用的第二个参数是默认值True。
1 Var Solver::newVar(bool sign, bool dvar) //该函数第二个参数默认值为true
2 {
3 int v = nVars();
4
5 //--------------------------------
6 // Update on 2020-03-10
7 // node created for var graph
8 varGraph->AddNode(v); // Update on 2020-01-04 //只考虑正文字索引， 负文字索引加1等于正文字的索引
9 varCmt.push(-1); // Update on 2020-01-04 //初始化变元所在的社区值为-1
10 //--------------------------------
11
12 watches_bin.init(mkLit(v, false));
13 watches_bin.init(mkLit(v, true ));
14 watches .init(mkLit(v, false));
15 watches .init(mkLit(v, true ));
16 assigns .push(l_Undef);
17 vardata .push(mkVarData(CRef_Undef, 0));
18 activity_CHB .push(0);
19 activity_VSIDS.push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
20
21 picked.push(0);
22 conflicted.push(0);
23 almost_conflicted.push(0);
24 #ifdef ANTI_EXPLORATION
25 canceled.push(0);
26 #endif
27
28 seen .push(0);
29 seen2 .push(0);
30 polarity .push(sign);
31 decision .push();
32 trail .capacity(v+1);
33 setDecisionVar(v, dvar); //默认参数dvar值默认为true
34
35 activity_distance.push(0);
36 var_iLevel.push(0);
37 var_iLevel_tmp.push(0);
38 pathCs.push(0);
39 40
41 return v;
42 }
|
|
1 inline void Solver::setDecisionVar(Var v, bool b)
2 {
3 if ( b && !decision[v]) dec_vars++;
4 else if (!b && decision[v]) dec_vars--;
5
6 decision[v] = b;
7 if (b && !order_heap_CHB.inHeap(v)){
8 order_heap_CHB.insert(v);
9 order_heap_VSIDS.insert(v);
10 order_heap_distance.insert(v);}
11 }
可以看到，采用默认参数b为真，则 （1） decision[v] = b； 该变元可以作为决策变元使用； |
|