Trait VariableSelection

Source

pub trait VariableSelection<L: Literal>: Debug + Clone {
    // Required methods
    fn new<C: AsRef<[L]>>(num_vars: usize, vars: &[L], clauses: &[C]) -> Self;
    fn pick<A: Assignment>(&mut self, assignment: &A) -> Option<L>;
    fn bumps<T: IntoIterator<Item = L>>(&mut self, vars: T);
    fn decay(&mut self, decay: f64);
    fn decisions(&self) -> usize;
}

Expand description

Trait defining the interface for variable selection strategies.

Implementors of this trait decide which unassigned variable to choose next for a decision and, implicitly or explicitly, which polarity to assign to it.

§Type Parameters

L: The Literal type used by the solver.

Required Methods§

Source

fn new<C: AsRef<[L]>>(num_vars: usize, vars: &[L], clauses: &[C]) -> Self

Creates a new instance of the variable selection strategy.

§Parameters

num_vars: The total number of variables in the SAT problem.
vars: A slice of all literals (often used for initial setup, though not all strategies use it).
clauses: A slice of clauses in the SAT problem. Some strategies use this to initialise scores.

Source

fn pick<A: Assignment>(&mut self, assignment: &A) -> Option<L>

Picks an unassigned variable for the next decision.

Returns Some(L) with the chosen literal (variable and its assigned polarity) if an unassigned variable can be found. Returns None if all variables relevant to the strategy are assigned.

§Parameters

assignment: The current state of variable assignments in the solver.

Source

fn bumps<T: IntoIterator<Item = L>>(&mut self, vars: T)

Increases the activity score of the specified variables.

This is called when a conflict is analysed, and the variables involved in the conflict (or the learned clause) are “rewarded”.

§Parameters

vars: An iterator over literals whose activity should be bumped.

Source

fn decay(&mut self, decay: f64)

Decays the activity scores of all variables.

This is periodically called to give more weight to recently active variables. The exact mechanism can vary (e.g. multiplying all scores by a factor, or increasing an activity increment).

§Parameters

decay: The decay factor. The interpretation of this factor depends on the specific strategy. For VSIDS-like strategies, it’s typically a value slightly less than 1 (e.g. 0.95), and activity_inc is divided by this factor.

Source