splr/assign/
learning_rate.rs

1/// Var Rewarding based on Learning Rate Rewarding and Reason Side Rewarding
2use {
3    super::{AssignStack, Var},
4    crate::types::*,
5};
6
7impl ActivityIF<VarId> for AssignStack {
8    #[inline]
9    fn activity(&self, vi: VarId) -> f64 {
10        self.var[vi].reward
11    }
12    // fn activity_slow(&self, vi: VarId) -> f64 {
13    //     self.var[vi].reward_ema.get()
14    // }
15    fn set_activity(&mut self, vi: VarId, val: f64) {
16        self.var[vi].reward = val;
17    }
18    fn reward_at_analysis(&mut self, vi: VarId) {
19        self.var[vi].turn_on(FlagVar::USED);
20    }
21    #[inline]
22    fn reward_at_assign(&mut self, _vi: VarId) {}
23    #[inline]
24    fn reward_at_propagation(&mut self, _vi: VarId) {}
25    #[inline]
26    fn reward_at_unassign(&mut self, vi: VarId) {
27        self.var[vi].update_activity(self.activity_decay, self.activity_anti_decay);
28    }
29    fn update_activity_decay(&mut self, scaling: f64) {
30        self.activity_decay = scaling;
31        self.activity_anti_decay = 1.0 - scaling;
32    }
33    // Note: `update_rewards` should be called before `cancel_until`
34    #[inline]
35    fn update_activity_tick(&mut self) {
36        self.tick += 1;
37    }
38}
39
40impl AssignStack {
41    pub fn rescale_activity(&mut self, scaling: f64) {
42        for v in self.var.iter_mut().skip(1) {
43            v.reward *= scaling;
44        }
45    }
46    // pub fn set_activity_trend(&mut self) -> f64 {
47    //     let mut nv = 0;
48    //     let mut inc = 0;
49    //     let mut activity_sum: f64 = 0.0;
50    //     // let mut dec = 1;
51    //     for (vi, v) in self.var.iter_mut().enumerate().skip(1) {
52    //         if v.is(FlagVar::ELIMINATED) || self.level[vi] == self.root_level {
53    //             continue;
54    //         }
55    //         nv += 1;
56    //         activity_sum += v.reward;
57    //         let trend = v.reward_ema.trend();
58    //         if 1.0 < trend {
59    //             inc += 1;
60    //         }
61    //     }
62    //     self.activity_averaged = activity_sum / nv as f64;
63    //     self.cwss = inc as f64 / nv as f64;
64    //     // println!("inc rate:{:>6.4}", self.cwss);
65    //     self.cwss
66    // }
67}
68
69impl Var {
70    fn update_activity(&mut self, decay: f64, reward: f64) -> f64 {
71        // Note: why the condition can be broken.
72        //
73        // 1. asg.ordinal += 1;
74        // 1. handle_conflict -> cancel_until -> reward_at_unassign
75        // 1. assign_by_implication -> v.timestamp = asg.ordinal
76        // 1. restart
77        // 1. cancel_until -> reward_at_unassign -> assertion failed
78        //
79        self.reward *= decay;
80        if self.is(FlagVar::USED) {
81            self.reward += reward;
82            self.turn_off(FlagVar::USED);
83        }
84        // self.reward_ema.update(self.reward);
85        self.reward
86    }
87}
splr/assign/learning_rate.rs

splr/assign/
learning_rate.rs
