Skip to main content

pumpkin_core/propagators/nogoods/
learning_options.rs

1use crate::propagation::Priority;
2
3/// Options related to nogood management, i.e., how and when to remove learned nogoods from the
4/// database.
5#[derive(Debug, Copy, Clone)]
6pub struct LearningOptions {
7    /// Determines when to rescale the activites of the learned nogoods in the database.
8    pub max_activity: f32,
9    /// Determines the factor by which the activities are divided when a conflict is found.
10    pub activity_decay_factor: f32,
11    /// The solver partitions the nogoods into three tiers.
12    ///
13    /// This limit specifies how many nogoods can be stored in the "high" LBD tier.
14    pub max_num_high_lbd_nogoods: usize,
15    /// The solver partitions the nogoods into three tiers.
16    ///
17    /// This limit specifies how many nogoods can be stored in the "mid" LBD tier.
18    pub max_num_mid_lbd_nogoods: usize,
19    /// The solver partitions the nogoods into three tiers.
20    ///
21    /// This limit specifies how many nogoods can be stored in the "low" LBD tier.
22    pub max_num_low_lbd_nogoods: usize,
23    /// Used to determine which tier a nogood belongs in.
24    ///
25    /// If the LBD of a nogood is higher than or equal to this threshold then it is considered to
26    /// be a "high" LBD nogood.
27    ///
28    /// If the LBD of a nogood is between [`LearningOptions::lbd_threshold_high`] and
29    /// [`LearningOptions::lbd_threshold_low`] then it is considered a "mid" LBD nogood.
30    pub lbd_threshold_high: u32,
31    /// Used to determine which tier a nogood belongs in.
32    ///
33    /// If the LBD of a nogood is lower than or equal to this value then it is considered to be a
34    /// "low" LBD nogood.
35    ///
36    /// If the LBD of a nogood is between [`LearningOptions::lbd_threshold_high`] and
37    /// [`LearningOptions::lbd_threshold_low`] then it is considered a "mid" LBD nogood.
38    pub lbd_threshold_low: u32,
39    /// Specifies by how much the activity is increased when a nogood is bumped.
40    pub activity_bump_increment: f32,
41    /// The priority of the nogood propagator.
42    pub nogood_propagator_priority: Priority,
43}
44impl Default for LearningOptions {
45    fn default() -> Self {
46        Self {
47            max_activity: 1e20,
48            activity_decay_factor: 0.99,
49            max_num_high_lbd_nogoods: 20000,
50            max_num_mid_lbd_nogoods: 7000,
51            max_num_low_lbd_nogoods: 100000,
52            lbd_threshold_high: 7,
53            lbd_threshold_low: 3,
54            activity_bump_increment: 1.0,
55            nogood_propagator_priority: Priority::High,
56        }
57    }
58}