代码解读——Solver.h及Solver.cpp

 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； 该变元可以作为决策变元使用；
（2） 该变元加入各种计算活跃度的堆中，参与排序；

如果，某些变元的赋值值已知，则newVars函数中可以不采用默认参数，或求解器内在求解过程中途通过
调用专门的设置函数，将变元v的decision[v]设置为假，并从各个堆中去除v，并在赋值序列中固定其赋值。