CadicalにCHBを実装

 CHBの実装をコパイに依頼したら、次のコードを提示されました。

int Internal::pick_chb_branch_lit () {
  double best = -1.0;
  int best_idx = 0;

  // 変数集合のイテレーション：CaDiCaL の実装に合わせて調整
  for (int idx = 2; idx <= max_var; idx++) { // idx: internal literal index (±)
    if (!active (idx)) continue;
    if (val (idx)) continue;          // すでに割り当て済み

    const double s = chb_score (idx);
    if (s > best) {
      best = s;
      best_idx = idx;
    }
  }
}

これは、却下です。変数の全スコアをスキャンして、その最高値を持ってくる実装ですが、遅すぎて話になりません。折角、スコア用のヒープを備えているのですから、それを利用しない手はありません。

struct score_smaller {
  Internal * internal;
  score_smaller (Internal * i) : internal (i) { }
  bool operator () (unsigned a, unsigned b);
};
struct ScoreComparator {//FEB042026
    Internal* internal;
    ScoreComparator(Internal* i) : internal(i) {}
    // ここが比較の核心：internal->score (a) の値を直接見ている
    bool operator () (unsigned a, unsigned b)const;

};
typedef heap ScoreSchedule;
typedef heap ScoreHeap;//FEB042026

#ifdef USE_CHB
inline bool ScoreComparator::operator() (unsigned a, unsigned b) const {
    assert(1 <= a);
    assert(a <= (unsigned)internal->max_var);
    assert(1 <= b);
    assert(b <= (unsigned)internal->max_var);
    return internal->chb_score(a) < internal->chb_score(b);
}

#endif
#ifdef USE_CHB
  double& chb_score(int lit) { return chb[vidx(lit)]; }
#endif
void Internal::bump_variable_score (int lit) {
  assert (opts.bump);
  int idx = vidx (lit);

#ifdef USE_CHB
  
  const int64_t conflicts = stats.conflicts;

  // CHBの報酬計算: 1 / (現在のコンフリクト番号 - 最後にこの変数が関与した番号 + 1)
  double reward = 1.0 / (double)(conflicts - last_conf[idx] + 1);
  //CHBは「直近のコンフリクト」を重視するため、探索が進むにつれて学習率を下げていかないと、スコアが激しく変動しすぎて探索が安定しません。 Liangらの論文で推奨されている標準的な設定は以下の通り： 初期値(\(\alpha _{ start }\)) : 0.4下限値(\(\alpha _{ min }\)) : 0.06減衰量(\(\alpha _{ step }\)) : 1e-6（衝突1回につき）
  if (chb_alpha > 0.06) {
      chb_alpha -= 0.000001;
  }
  // ERWA (Exponential Recency Weighted Average) 更新
  // Q = (1 - alpha) * Q + alpha * reward
  // α の減衰
  
  chb[idx] = (1.0 - chb_alpha) * chb[idx] + chb_alpha * reward;
  last_conf[idx] = conflicts;

  // ヒープの更新（ScoreComparatorがchbを参照するようになっているため、これで並び替わる）
  if (chb_scores.contains(idx)) chb_scores.update(idx);


#endif

Liangさんの論文に示された通りの実装にしています。上の更新式は、一次IIRフィルタに似ています。

当時、確か、機械学習の発想を取り入れた、との話があったかに記憶しています。

https://ojs.aaai.org/index.php/AAAI/article/view/10439

なお、CHBは、VSIDSよりもリスタート間隔を短くした方がよい、という説もありますが、真偽は分かりません。

Combining VSIDS and CHB Using Restarts in SAT

Cadical/Kissa共、CHBを実装していないのですが、最近のSAT competitioin優勝ソルバは、いずれもMAB方式です。

A new variable ordering for in-processing bounded variable elimination in SAT solvers | Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence