csp_solver/solver/
restart.rs

1//! Luby restart schedule.
2//!
3//! The Luby sequence `1,1,2,1,1,2,4,1,1,2,1,1,2,4,8,…` is log-optimal for
4//! restarting a Las-Vegas algorithm whose runtime distribution is unknown
5//! (Luby, Sinclair & Zuckerman 1993) — the canonical CSP/SAT cure for
6//! heavy-tailed search. The i-th run is given a conflict budget of
7//! `luby(i) · unit`; on exhaustion the search unwinds to the root and
8//! re-descends, *retaining* the CHS weights, phase memory, and restart
9//! nogoods accumulated so far (otherwise a restart merely repeats itself).
10//!
11//! Values are produced by Knuth's "reluctant doubling" recurrence — O(1) per
12//! step, no table, no recursion.
13
14/// Default per-restart base unit, in conflicts. The k-th run runs for
15/// `luby(k) · UNIT` conflicts before cutting off.
16pub const DEFAULT_UNIT: u64 = 100;
17
18/// Streaming generator for the Luby unit sequence.
19#[derive(Debug, Clone)]
20pub struct Luby {
21    u: u64,
22    v: u64,
23}
24
25impl Luby {
26    /// Fresh generator positioned before the first term.
27    pub fn new() -> Self {
28        Self { u: 1, v: 1 }
29    }
30
31    /// Next term of the Luby sequence.
32    #[inline]
33    pub fn next_term(&mut self) -> u64 {
34        let term = self.v;
35        if self.u & self.u.wrapping_neg() == self.v {
36            self.u += 1;
37            self.v = 1;
38        } else {
39            self.v *= 2;
40        }
41        term
42    }
43}
44
45impl Default for Luby {
46    fn default() -> Self {
47        Self::new()
48    }
49}
50
51impl Iterator for Luby {
52    type Item = u64;
53    #[inline]
54    fn next(&mut self) -> Option<u64> {
55        Some(self.next_term())
56    }
57}
csp_solver/solver/restart.rs

csp_solver/solver/
restart.rs
