Struct Vsids

pub struct Vsids<Var: StorageKey> { /* private fields */ }

A VariableSelector which implements VSIDS [1].

This selctor determines which variables should be branched on based on how often it appears in conflicts.

Intuitively, the more often a variable appears in recent conflicts, the more “important” it is during the search process.

VSIDS is originally from the SAT field (see [1]) but we adapted it here to work on integer variables as well. There are some details which do not necessarily translate 1-to-1; for example, during conflict analysis the activity of an integer variable can be bumped multiple times if multiple literals related to it are encountered.

Bibliography

[1] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, ‘Chaff: Engineering an efficient SAT solver’, in Proceedings of the 38th annual Design Automation Conference, 2001, pp. 530–535.

Implementations

impl<Var: StorageKey + Clone + Copy> Vsids<Var>

pub fn new(variables: &[Var]) -> Self

Creates a new instance of the Vsids VariableSelector with certain default values for the parameters (1.0 for the increment, 1e100 for the max threshold, 0.95 for the decay factor and 0.0 for the initial VSIDS value).

pub fn with_initial_values(variables: &[Var], initial_values: &[f64]) -> Self

Creates a new instance of the Vsids VariableSelector with certain default values for the parameters (1.0 for the increment, 1e100 for the max threshold and 0.95 for the decay factor). It initialises the internal max-heap structure used for finding the maximum Var with the provided initial_values; this parameter can thus be used to guide the early search process of the selector.

It is required that the length of variables is equal to the length of initial_values.

Trait Implementations

impl<Var: Debug + StorageKey> Debug for Vsids<Var>

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

Formats the value using the given formatter.

impl VariableSelector<DomainId> for Vsids<DomainId>

fn select_variable( &mut self, context: &SelectionContext<'_>, ) -> Option<DomainId>

Determines which variable to select next if there are any left to branch on. Should only return None when all variables which have been passed to the VariableSelector have been assigned. Otherwise it should return the variable to branch on next.

fn on_conflict(&mut self)

A function which is called after a conflict has been found and processed but (currently) does not provide any additional information.

fn on_unassign_integer(&mut self, variable: DomainId, _value: i32)

A function which is called after a DomainId is unassigned during backtracking (i.e. when it was fixed but is no longer), specifically, it provides variable which is the DomainId which has been reset. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_appearance_in_conflict_integer(&mut self, variable: DomainId)

A function which is called when a variable appears in a conflict during conflict analysis.

fn is_restart_pointless(&mut self) -> bool

This method returns whether a restart is currently pointless for the VariableSelector.

fn on_unassign_literal(&mut self, _literal: Literal)

A function which is called after a Literal is unassigned during backtracking (i.e. when it was fixed but is no longer), specifically, it provides literal which is the Literal which has been reset. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_appearance_in_conflict_literal(&mut self, _literal: Literal)

A function which is called when a Literal appears in a conflict during conflict analysis.

impl VariableSelector<PropositionalVariable> for Vsids<PropositionalVariable>

fn select_variable( &mut self, context: &SelectionContext<'_>, ) -> Option<PropositionalVariable>

Determines which variable to select next if there are any left to branch on. Should only return None when all variables which have been passed to the VariableSelector have been assigned. Otherwise it should return the variable to branch on next.

fn on_conflict(&mut self)

A function which is called after a conflict has been found and processed but (currently) does not provide any additional information.

fn on_unassign_literal(&mut self, literal: Literal)

A function which is called after a Literal is unassigned during backtracking (i.e. when it was fixed but is no longer), specifically, it provides literal which is the Literal which has been reset. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_appearance_in_conflict_literal(&mut self, literal: Literal)

A function which is called when a Literal appears in a conflict during conflict analysis.

fn is_restart_pointless(&mut self) -> bool

This method returns whether a restart is currently pointless for the VariableSelector.

fn on_unassign_integer(&mut self, _variable: DomainId, _value: i32)

A function which is called after a DomainId is unassigned during backtracking (i.e. when it was fixed but is no longer), specifically, it provides variable which is the DomainId which has been reset. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_appearance_in_conflict_integer(&mut self, _variable: DomainId)

A function which is called when a variable appears in a conflict during conflict analysis.