1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177

use crate::config::Config;
use crate::traits::*;
use crate::types::Ema;

// const RESET_EMA: usize = 400;

#[derive(Debug)]
pub struct ProgressASG {
    asg: usize,
    ema: Ema,
    /// For block restart based on average assignments: 1.40.
    /// This is called `R` in Glucose
    pub threshold: f64,
}

impl ProgressEvaluator for ProgressASG {
    type Input = usize;
    fn update(&mut self, n: usize) {
        self.asg = n;
        self.ema.update(n as f64);
    }
    fn get(&self) -> f64 {
        self.ema.get()
    }
    fn trend(&self) -> f64 {
        (self.asg as f64) / self.ema.get()
    }
    fn is_active(&self) -> bool {
        self.threshold * self.ema.get() < (self.asg as f64)
    }
    fn new(config: &Config) -> Self {
        ProgressASG {
            ema: Ema::new(config.restart_asg_len),
            asg: 0,
            threshold: config.restart_blocking,
        }
    }
}

#[derive(Debug)]
pub struct ProgressLBD {
    ema: Ema,
    num: usize,
    sum: usize,
    /// For force restart based on average LBD of newly generated clauses: 0.80.
    /// This is called `K` in Glucose
    pub threshold: f64,
}

impl ProgressEvaluator for ProgressLBD {
    type Input = usize;
    fn update(&mut self, d: usize) {
        self.num += 1;
        self.sum += d;
        self.ema.update(d as f64);
    }
    fn get(&self) -> f64 {
        self.ema.get()
    }
    fn trend(&self) -> f64 {
        self.ema.get() * (self.num as f64) / (self.sum as f64)
    }
    fn is_active(&self) -> bool {
        (self.sum as f64) < self.ema.get() * (self.num as f64) * self.threshold
    }
    fn new(config: &Config) -> Self {
        ProgressLBD {
            ema: Ema::new(config.restart_lbd_len),
            num: 0,
            sum: 0,
            threshold: config.restart_threshold,
        }
    }
}

// Restart stat
#[derive(Debug)]
pub struct RestartExecutor {
    pub adaptive_restart: bool,
    pub asg: ProgressASG,
    pub lbd: ProgressLBD,
    pub use_luby_restart: bool,
    pub after_restart: usize,
    pub cur_restart: usize,
    pub next_restart: usize,
    pub restart_step: usize,
    luby_count: f64,
    pub luby_restart_num_conflict: f64,
    pub luby_restart_inc: f64,
    pub luby_current_restart: usize,
    pub luby_restart_factor: f64,
}

impl RestartIF for RestartExecutor {
    fn new(config: &Config) -> Self {
        RestartExecutor {
            adaptive_restart: !config.without_adaptive_restart,
            asg: ProgressASG::new(config),
            lbd: ProgressLBD::new(config),
            use_luby_restart: false,
            after_restart: 0,
            cur_restart: 1,
            next_restart: 100,
            restart_step: config.restart_step,
            luby_count: 0.0,
            luby_restart_num_conflict: 0.0,
            luby_restart_inc: 2.0,
            luby_current_restart: 0,
            luby_restart_factor: 100.0,
        }
    }
    fn block_restart(&mut self) -> bool {
        if 100 < self.lbd.num
            && !self.use_luby_restart
            && self.restart_step <= self.after_restart
            && self.asg.is_active()
        {
            self.after_restart = 0;
            return true;
        }
        false
    }
    fn force_restart(&mut self) -> bool {
        if (self.use_luby_restart && self.luby_restart_num_conflict <= self.luby_count)
            || (!self.use_luby_restart
                && self.restart_step <= self.after_restart
                && self.lbd.is_active())
        {
            self.after_restart = 0;
            if self.use_luby_restart {
                self.luby_count = 0.0;
                self.luby_current_restart += 1;
                self.luby_restart_num_conflict =
                    luby(self.luby_restart_inc, self.luby_current_restart)
                        * self.luby_restart_factor;
            }
            return true;
        }
        false
    }
    fn initialize_luby(&mut self) {
        if self.use_luby_restart {
            self.luby_restart_num_conflict =
                luby(self.luby_restart_inc, self.luby_current_restart) * self.luby_restart_factor;
            self.luby_count = 0.0;
        }
    }
    fn update_luby(&mut self) {
        if self.use_luby_restart {
            self.luby_count += 1.0;
        }
    }
}

/// Find the finite subsequence that contains index 'x', and the
/// size of that subsequence:
fn luby(y: f64, mut x: usize) -> f64 {
    let mut size: usize = 1;
    let mut seq: usize = 0;
    // for(size = 1, seq = 0; size < x + 1; seq++, size = 2 * size + 1);
    while size < x + 1 {
        seq += 1;
        size = 2 * size + 1;
    }
    // while(size - 1 != x) {
    //     size = (size - 1) >> 1;
    //     seq--;
    //     x = x % size;
    // }
    while size - 1 != x {
        size = (size - 1) >> 1;
        seq -= 1;
        x %= size;
    }
    // return pow(y, seq);
    y.powf(seq as f64)
}