nandaro

VSIDS は Variable State Independent Decaying Sum の略。
2001 年に Chaff で用いられてから、2011年の現在に至るまで多くの SAT ソルバに利用されているヒューリスティクスである。
変数毎に出現頻度を表すactivityというカウンタを用いる。

• 学習した節に含まれる変数のカウンタを増やす
• 一定時間ごとに全ての変数のカウンタを減らす

このようにして、効率的な変数選択を行う。
ここで、MiniSat2.2 の変数選択フェーズである関数 pickBranchLit() を見てみよう。

 
Lit Solver::pickBranchLit()
{
    Var next = var_Undef;

    // Random decision:
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
        next = order_heap[irand(random_seed,order_heap.size())];
        if (value(next) == l_Undef && decision[next])
            rnd_decisions++; }

    // Activity based decision:
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
        if (order_heap.empty()){
            next = var_Undef;
            break;
        }else
            next = order_heap.removeMin();

    return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : polarity[next]);
}

実は MiniSat2.0 で行われていた 2% のランダム選択は MiniSat2.2 のデフォルト設定では一切行われない。
ということでランダム選択のところは忘れよう。

あと、最後の return 文で rnd_pol という bool 変数があるが、これもデフォルトでは値が false なので、ここでは考えないことにしよう。

先程のコードから当該箇所を除いて、コメントを勝手に追加するとこんな感じになる。

 
Lit Solver::pickBranchLit() //リテラル (構造体 Lit) を返す
{
    Var next = var_Undef;

    // Activity based decision:
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
        // 変数が選択されていないか、値が未定か、選択した変数がdecisionしてはいけないものか
        if (order_heap.empty()){ 
            next = var_Undef;              //未定変数が無い (つまり、探索終了)
            break;
        }else
            next = order_heap.removeMin(); //変数は利用頻度順にヒープに格納されてる

    return next == var_Undef ? lit_Undef : mkLit(next, polarity[next]);
}

最後の mkLit() という関数の第 2 引数に polarity という配列があるが、
この配列は各変数に true を割り当てるか false を割り当てるかを保持している。
予め polarity の全ての要素は false が格納されている。
つまり、MiniSat2.2 は普段は未定変数に false を割り当てることになる。
ただし、後述の Phase Saving 機能を有効にしてたりするとその限りではない。