Expand description
Conflict-history weighting (CHS / ERWA) for dynamic variable ordering.
Replaces the frozen constraint_weights ≡ 1.0 (which is why Ordering::Mrv
reduces to plain min-remaining-value) with an exponential recency-weighted
average per constraint, following Habet & Terrioux’s Conflict-History
Search (CHS, J. Heuristics 2021).
On every conflict (a failed check or a propagation domain wipe-out) the
offending constraint c is bumped:
r = 1 / (conflicts − last_conflict[c] + 1)
q[c] ← (1 − α)·q[c] + α·r
α ← max(α_min, α − α_decay) (decays 0.4 → 0.06)Branching then minimises dom(x) / Σ_{c ∈ scope(x)} q[c] — constraints
that failed recently and often dominate the denominator, pulling their
variables to the front of the search.
Weights are search-only state: they never touch the BBNF monotonic / lattice propagation path (which never enters backtracking search).
Structs§
- Conflict
History - Dynamic conflict-history state threaded through backtracking search.