Struct LearningOptions

pub struct LearningOptions {
    pub max_clause_activity: f32,
    pub clause_activity_decay_factor: f32,
    pub num_high_lbd_learned_clauses_max: u64,
    pub high_lbd_learned_clause_sorting_strategy: LearnedClauseSortingStrategy,
    pub lbd_threshold: u32,
}

Options which determine how the learned clauses are handled within the Solver. These options influence when the learned clause database removed clauses.

Fields

max_clause_activity: f32

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

clause_activity_decay_factor: f32

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

num_high_lbd_learned_clauses_max: u64

The maximum number of clauses with an LBD higher than LearningOptions::lbd_threshold allowed by the learned clause database. If there are more clauses with an LBD higher than LearningOptions::lbd_threshold then removal from the database will be considered.

high_lbd_learned_clause_sorting_strategy: LearnedClauseSortingStrategy

Specifies how the learned clauses are sorted when considering removal.

lbd_threshold: u32

The treshold which specifies whether a learned clause database is considered to be with “High” LBD or “Low” LBD. Learned clauses with high LBD will be considered for removal.

Trait Implementations

impl Clone for LearningOptions

fn clone(&self) -> LearningOptions

Returns a copy 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

Formats the value using the given formatter.

impl Default for LearningOptions

fn default() -> Self

Returns the “default value” for a type.

impl Copy for LearningOptions