Struct PhaseSaving

pub struct PhaseSaving<Var, Value: PartialEq> { /* private fields */ }

A ValueSelector which implements phase-saving.

During the search process, values of variables are saved whenever they are assigned and the search process will attempt to assign to these values whenever possible. After a variable has been fixed, its value will be saved as the previous value and the search will continue. Values can be frozen meaning that they will not be updated with the previously assigned value during the search process, provided initial values will always be frozen.

Bibliography

[1] K. Pipatsrisawat and A. Darwiche, ‘A lightweight component caching scheme for satisfiability solvers’, in Theory and Applications of Satisfiability Testing–SAT 2007: 10th International Conference, Lisbon, Portugal, May 28-31, 2007. Proceedings 10, 2007, pp. 294–299.

Implementations

impl PhaseSaving<PropositionalVariable, bool>

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

Creates a new instance of PhaseSaving over PropositionalVariables with false as its default value.

impl<Var: StorageKey + Copy + PartialEq, Value: Copy + PartialEq> PhaseSaving<Var, Value>

pub fn with_default_value(variables: &[Var], default_value: Value) -> Self

Constructor for creating the PhaseSaving ValueSelector with a default value; the default value will be the selected value if no value is saved for the provided variable

pub fn with_initial_values( variables: &[Var], variables_with_initial_value: Vec<(Var, Value)>, default_value: Value, ) -> Self

Constructor for creating the PhaseSaving ValueSelector with initial values (and a default value); if no value is saved then the provided initial value is selected and otherwise the default value is selected.

It is possible to provide fewer values than number of variables but it is required that every variable present in variables_with_initial_value is also present in variables.

pub fn freeze(&mut self, variable: Var, new_value: Value)

Freeze the value of the provided variable

Trait Implementations

impl<Var: Debug, Value: Debug + PartialEq> Debug for PhaseSaving<Var, Value>

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

Formats the value using the given formatter.

impl ValueSelector<PropositionalVariable> for PhaseSaving<PropositionalVariable, bool>

fn select_value( &mut self, _: &mut SelectionContext<'_>, decision_variable: PropositionalVariable, ) -> Predicate

Determines which value in the domain of decision_variable to branch next on. The domain of the decision_variable variable should have at least 2 values in it (as it otherwise should not have been selected as decision_variable). Returns a Predicate specifying the required change in the domain.

fn on_unassign_literal(&mut self, lit: 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 is_restart_pointless(&mut self) -> bool

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

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 and value which is the value to which the variable was previously fixed. This method could thus be called multiple times in a single backtracking operation by the solver.

fn on_solution(&mut self, _solution: SolutionReference<'_>)

This method is called when a solution is found; either when iterating over all solutions in the case of a satisfiable problem or on solutions of increasing quality when solving an optimisation problem.