splr 0.17.0

A modern CDCL SAT solver in Rust
Documentation 
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

/// Var Rewarding based on EVSIDS
use {
    super::{AssignStack, Var},
    crate::types::*,
};

impl ActivityIF<VarId> for AssignStack {
    fn activity(&self, vi: VarId) -> f64 {
        self.var[vi].reward
    }
    fn set_activity(&mut self, vi: VarId, val: f64) {
        self.var[vi].reward = val;
    }
    fn reward_at_analysis(&mut self, vi: VarId) {
        let s = self.activity_decay_step;
        let t = self.ordinal;
        let v = &mut self.var[vi];
        if v.timestamp == t {
            return;
        }
        v.timestamp = t;
        v.reward += s;
        const SCALE: f64 = 1e-100;
        const SCALE_MAX: f64 = 1e100;
        if SCALE_MAX < v.reward {
            for v in &mut self.var[1..] {
                v.reward *= SCALE;
            }
            self.activity_decay_step *= SCALE;
        }
    }
    fn update_activity_decay(&mut self, _: f64) {
        self.activity_decay = self
            .activity_decay_default
            .min(self.activity_decay + self.activity_decay_step);
        self.activity_anti_decay = 1.0 - self.activity_decay;
    }
    fn update_activity_tick(&mut self) {
        const INC_SCALE: f64 = 1.01;
        if self.ordinal == 0 {
            self.activity_decay *= 0.5;
            self.activity_anti_decay = 1.0 - self.activity_decay;
        }
        self.ordinal += 1;
        self.activity_decay_step *= INC_SCALE;
    }
}