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

//! Solver configuration.
use varisat_internal_macros::{ConfigUpdate, DocDefault};

/// Configurable parameters used during solving.
#[derive(DocDefault, ConfigUpdate)]
pub struct SolverConfig {
    /// Multiplicative decay for the VSIDS decision heuristic.
    ///
    /// [default: 0.95]  [range: 0.5..1.0]
    pub vsids_decay: f32,

    /// Multiplicative decay for clause activities.
    ///
    /// [default: 0.999]  [range: 0.5..1.0]
    pub clause_activity_decay: f32,

    /// Number of conflicts between local clause reductions.
    ///
    /// [default: 15000]  [range: 1..]
    pub reduce_locals_interval: u64,

    /// Number of conflicts between mid clause reductions.
    ///
    /// [default: 10000]  [range: 1..]
    pub reduce_mids_interval: u64,

    /// Scaling factor for luby sequence based restarts (number of conflicts).
    ///
    /// [default: 128]  [range: 1..]
    pub luby_restart_interval_scale: u64,
}