Revert to the original CHB or LRB about splr HOT 3 CLOSED

/// Called after a learnt clause is generated from conflict analysis
///  and before bracktrack.
fn after_conflict_analysis() {
  LEARNT_COUNT += 1;
  for v in conflict_side_vars + learnt_clause.vars {
    v.participated += 1;
  }
  // Reason Side Rate (RSR) extension
  for v in learnt_clause.vars.map(|v| v.reason).flatten() - learnt_clause.vars {
    v.reasoned += 1;
  }
  // locality extension
  for v in Vars {
    if !v.assign {
      v.Q *= 0.95;
    }
  }
  if 0.06 < 𝑎 {
    𝑎 -= 10E-6;
  }
}

/// Called when v is assigned by branching or propagation.
fn on_assign(v: Var) {
  v.assigned = LEARNT_COUNT;
  v.participated = 0;
  v.reasoned = 0;
}

/// Called when v is unassigned by backtracking or restart.
fn on_unassign(v: Var) {
  let interval = LEARNT_COUNT - v.assigned; // zero is possible due to restarts.
  if 0 < interval {
    let r = v.participated / interval;     // r is the Learning Rate (LR).
    let s = v.reasoned / interval;         // s is the RSL.
    v.Q = (1 - 𝑎) * v.Q + 𝑎 * (r + s);      // EMA style update.
  }
}