csp_solver/solver/
heuristic.rs

1//! Conflict-history weighting (CHS / ERWA) for dynamic variable ordering.
2//!
3//! Replaces the frozen `constraint_weights ≡ 1.0` (which is why `Ordering::Mrv`
4//! reduces to plain min-remaining-value) with an *exponential recency-weighted
5//! average* per constraint, following Habet & Terrioux's Conflict-History
6//! Search (CHS, J. Heuristics 2021).
7//!
8//! On every conflict (a failed check or a propagation domain wipe-out) the
9//! offending constraint `c` is bumped:
10//!
11//! ```text
12//! r        = 1 / (conflicts − last_conflict[c] + 1)
13//! q[c]     ← (1 − α)·q[c] + α·r
14//! α        ← max(α_min, α − α_decay)      (decays 0.4 → 0.06)
15//! ```
16//!
17//! Branching then minimises `dom(x) / Σ_{c ∈ scope(x)} q[c]` — constraints
18//! that failed recently and often dominate the denominator, pulling their
19//! variables to the front of the search.
20//!
21//! Weights are *search-only* state: they never touch the BBNF monotonic /
22//! lattice propagation path (which never enters backtracking search).
23
24/// Initial per-constraint score. Starting at `1.0` (rather than CHS's `0.0`)
25/// makes the denominator `Σ q` behave like weighted-degree on the first
26/// descent — i.e. MRV on a degree-uniform graph such as sudoku — before any
27/// conflict has been observed, avoiding the divide-by-near-zero degeneracy of
28/// a cold `q ≡ 0` start. Once conflicts accrue the ERWA update takes over.
29const INITIAL_Q: f64 = 1.0;
30
31/// Starting ERWA step size (favours recent conflicts heavily).
32const ALPHA_INIT: f64 = 0.4;
33/// Per-conflict decay applied to `α`.
34const ALPHA_DECAY: f64 = 1e-6;
35/// Floor for `α` (long-run smoothing factor).
36const ALPHA_MIN: f64 = 0.06;
37
38/// Dynamic conflict-history state threaded through backtracking search.
39#[derive(Debug, Clone)]
40pub struct ConflictHistory {
41    /// `q[c]` — CHS score per constraint. Read by `Ordering::{Chs,Mrv}`.
42    weights: Vec<f64>,
43    /// `last_conflict[c]` — global conflict count at `c`'s previous failure.
44    last_conflict: Vec<u64>,
45    /// Global conflict counter (monotonic across restarts).
46    conflicts: u64,
47    /// Current ERWA step size.
48    alpha: f64,
49    /// When `false`, `bump` is a no-op and weights stay at `INITIAL_Q`
50    /// (keeps the frozen-weight `Mrv` scan for non-CHS orderings).
51    enabled: bool,
52}
53
54impl ConflictHistory {
55    /// Create history for `num_constraints`. `enabled` gates the ERWA update;
56    /// when disabled the weights are the frozen `1.0` vector the pre-CHS code
57    /// used, so `Ordering::Mrv` stays bit-for-bit the frozen-weight scan.
58    pub fn new(num_constraints: usize, enabled: bool) -> Self {
59        Self {
60            weights: vec![INITIAL_Q; num_constraints],
61            last_conflict: vec![0; num_constraints],
62            conflicts: 0,
63            alpha: ALPHA_INIT,
64            enabled,
65        }
66    }
67
68    /// Create history seeded from an existing weight vector (e.g. the
69    /// `constraint_weights` built by `finalize()`). Behaves like `new` when
70    /// the seed is the conventional all-`1.0` vector.
71    pub fn from_seed(seed: &[f64], enabled: bool) -> Self {
72        Self {
73            weights: seed.to_vec(),
74            last_conflict: vec![0; seed.len()],
75            conflicts: 0,
76            alpha: ALPHA_INIT,
77            enabled,
78        }
79    }
80
81    /// Current weight vector, consumed by the ordering heuristic.
82    #[inline]
83    pub fn weights(&self) -> &[f64] {
84        &self.weights
85    }
86
87    /// Total conflicts recorded so far (used by the restart driver).
88    #[inline]
89    pub fn conflicts(&self) -> u64 {
90        self.conflicts
91    }
92
93    /// Register a conflict caused by constraint `ci` and apply the ERWA
94    /// update. A no-op when disabled.
95    #[inline]
96    pub fn bump(&mut self, ci: usize) {
97        if !self.enabled {
98            self.conflicts += 1;
99            return;
100        }
101        self.conflicts += 1;
102        let since = self.conflicts - self.last_conflict[ci] + 1;
103        let r = 1.0 / since as f64;
104        self.weights[ci] = (1.0 - self.alpha) * self.weights[ci] + self.alpha * r;
105        self.last_conflict[ci] = self.conflicts;
106        if self.alpha > ALPHA_MIN {
107            self.alpha = (self.alpha - ALPHA_DECAY).max(ALPHA_MIN);
108        }
109    }
110}
csp_solver/solver/heuristic.rs

csp_solver/solver/
heuristic.rs
