Struct LearningOptions 

pub struct LearningOptions {
    pub max_activity: f32,
    pub activity_decay_factor: f32,
    pub max_num_high_lbd_nogoods: usize,
    pub max_num_mid_lbd_nogoods: usize,
    pub max_num_low_lbd_nogoods: usize,
    pub lbd_threshold_high: u32,
    pub lbd_threshold_low: u32,
    pub activity_bump_increment: f32,
}

Options related to nogood management, i.e., how and when to remove learned nogoods from the database.

Fields

max_activity: f32

Determines when to rescale the activites of the learned nogoods in the database.

activity_decay_factor: f32

Determines the factor by which the activities are divided when a conflict is found.

max_num_high_lbd_nogoods: usize

The solver partitions the nogoods into three tiers.

This limit specifies how many nogoods can be stored in the “high” LBD tier.

max_num_mid_lbd_nogoods: usize

The solver partitions the nogoods into three tiers.

This limit specifies how many nogoods can be stored in the “mid” LBD tier.

max_num_low_lbd_nogoods: usize

The solver partitions the nogoods into three tiers.

This limit specifies how many nogoods can be stored in the “low” LBD tier.

lbd_threshold_high: u32

Used to determine which tier a nogood belongs in.

If the LBD of a nogood is higher than or equal to this threshold then it is considered to be a “high” LBD nogood.

If the LBD of a nogood is between LearningOptions::lbd_threshold_high and LearningOptions::lbd_threshold_low then it is considered a “mid” LBD nogood.

lbd_threshold_low: u32

Used to determine which tier a nogood belongs in.

If the LBD of a nogood is lower than or equal to this value then it is considered to be a “low” LBD nogood.

If the LBD of a nogood is between LearningOptions::lbd_threshold_high and LearningOptions::lbd_threshold_low then it is considered a “mid” LBD nogood.

activity_bump_increment: f32

Specifies by how much the activity is increased when a nogood is bumped.

Trait Implementations

impl Clone for LearningOptions

fn clone(&self) -> LearningOptions

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for LearningOptions

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for LearningOptions

fn default() -> LearningOptions

Returns the “default value” for a type.

impl Copy for LearningOptions