Struct RestartOptions 

pub struct RestartOptions {
    pub sequence_generator_type: SequenceGeneratorType,
    pub base_interval: u64,
    pub min_num_conflicts_before_first_restart: u64,
    pub lbd_coef: f64,
    pub num_assigned_coef: f64,
    pub num_assigned_window: u64,
    pub geometric_coef: Option<f64>,
    pub no_restarts: bool,
}

The options which are used by the solver to determine when a restart should occur.

An implementation of a restart strategy based on the specfication of Section 4 of [1] (for more information about the Glucose restart strategies see [2] and [3]). The idea is to restart when the the quality of the learned clauses (indicated by the LBD [4] which is the number of different decision levels present in a learned clause, lower is generally better) is poor. It takes this into account by keeping track of the overall average LBD and the short-term average LBD and comparing these with one another.

The strategy also takes into account that if a solver is “close” to finding a solution that it would be better to not restart at that moment and it can then decide to skip a restart.

It generalises the aforementioned Glucose restart strategy by using adjustable RestartOptions which allows the user to also specify Luby restarts (see [5]) and constant restarts (see Section 3 of [1]).

Bibliography

[1] A. Biere and A. Fröhlich, ‘Evaluating CDCL restart schemes’, Proceedings of Pragmatics of SAT, pp. 1–17, 2015.

[2] G. Audemard and L. Simon, ‘Refining restarts strategies for SAT and UNSAT’, in Principles and Practice of Constraint Programming: 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, 2012, pp. 118–126.

[3] G. Audemard and L. Simon, ‘Glucose 2.1: Aggressive, but reactive, clause database management, dynamic restarts (system description)’, in Pragmatics of SAT 2012 (POS’12), 2012.

[4] G. Audemard and L. Simon, ‘Predicting learnt clauses quality in modern SAT solvers’, in Twenty-first international joint conference on artificial intelligence, 2009.

[5] M. Luby, A. Sinclair, and D. Zuckerman, ‘Optimal speedup of Las Vegas algorithms’, Information Processing Letters, vol. 47, no. 4, pp. 173–180, 1993.

Fields

sequence_generator_type: SequenceGeneratorType

Decides the sequence based on which the restarts are performed. To be used in combination with RestartOptions::base_interval

base_interval: u64

The base interval length is used as a multiplier to the restart sequence. For example, constant restarts with base interval 100 means a retart is triggered every 100 conflicts.

min_num_conflicts_before_first_restart: u64

The minimum number of conflicts to be reached before the first restart is considered

lbd_coef: f64

Used to determine if a restart should be forced. The state is “bad” if the current LBD value is much greater than the global LBD average A greater/lower value for lbd-coef means a less/more frequent restart policy

num_assigned_coef: f64

Used to determine if a restart should be blocked. To be used in combination with RestartOptions::num_assigned_window. A restart is blocked if the number of assigned propositional variables is must greater than the average number of assigned variables in the recent past A greater/lower value for RestartOptions::num_assigned_coef means fewer/more blocked restarts

num_assigned_window: u64

Used to determine the length of the recent past that should be considered when deciding on blocking restarts. The solver considers the last RestartOptions::num_assigned_window conflicts as the reference point for the number of assigned variables

geometric_coef: Option<f64>

The coefficient in the geometric sequence x_i = x_{i-1} * geometric-coef where x_1 = RestartOptions::base_interval. Used only if RestartOptions::sequence_generator_type is assigned to SequenceGeneratorType::Geometric.

no_restarts: bool

Determines whether restarts should be able to occur

Trait Implementations

impl Clone for RestartOptions

fn clone(&self) -> RestartOptions

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RestartOptions

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

Formats the value using the given formatter.

impl Default for RestartOptions

fn default() -> RestartOptions

Returns the “default value” for a type.

impl Copy for RestartOptions