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，並在賦值序列中固定其賦值。