nandaro

Phase Saving とは、1 度割り当てた変数の割当を保持して使いまわす技術。
Phase Caching とか、Progress Saving と表現されることもある。

Phase Saving が嬉しいと言われる理由として、
「リスタートor非時間順バックトラックによって割当をキャンセルしても、
同じ変数に同じ割当をするケースが多い」ということが実験により知見として得られていることによる。
(リスタートとか非時間順バックトラックの話は後で)
要するに何度も同じところを解くのは止めようということ。

ソースを見てみよう。
バックトラックをする cancelUntil() 関数内で Phase Saving は行われている。

void Solver::cancelUntil(int level) {
  if (decisionLevel() > level){
    for (int c = trail.size()-1; c >= trail_lim[level]; c--){
      Var      x  = var(trail[c]);
      assigns [x] = l_Undef;
      if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) // Phase Saving が有効かどうか
        polarity[x] = sign(trail[c]);                                      // Phase Saving 実行。割当を保持
      insertVarOrder(x);
    }
    qhead = trail_lim[level];
    trail.shrink(trail.size() - trail_lim[level]);
    trail_lim.shrink(trail_lim.size() - level);
  }
}

ちょっと見にくいが、コメント付けてるあたりが該当箇所。
他のとこはたぶんバックトラックの話をするとこで触れるからスルー。

ちなみに、デフォルトだと phase_saving は 2 の full 設定になっている。
phase_saving を 0 (none) や 1 (limited) にして比較実験したところ、
2 の full が 1 番速かったみたい。