Struct Vsids

pub struct Vsids<const EARLY_EXIT: bool = false> { /* private fields */ }

A VSIDS (Variable State Independent Decaying Sum) implementation without a binary heap.

This strategy maintains an activity score for each literal. When picking a variable, it iterates through all literals to find the unassigned one with the highest score. This makes the pick operation O(N) where N is the number of variables.

EARLY_EXIT is a compile-time constant. If true, the pick operation may exit early if a literal with a sufficiently high score is found, potentially saving computation but possibly leading to suboptimal choices in some cases.

Trait Implementations

impl<const EARLY_EXIT: bool> Clone for Vsids<EARLY_EXIT>

fn clone(&self) -> Vsids<EARLY_EXIT>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const EARLY_EXIT: bool> Debug for Vsids<EARLY_EXIT>

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

Formats the value using the given formatter.

impl<const EARLY_EXIT: bool> Default for Vsids<EARLY_EXIT>

fn default() -> Vsids<EARLY_EXIT>

Returns the “default value” for a type.

impl<const E: bool> Index<usize> for Vsids<E>

Index trait implementation for the VSIDS variable selection strategy. Allows for indexing into the scores vector.

Safety

Should only be used internally and with care due to the unchecked indexing.

type Output = f64

The returned type after indexing.

fn index(&self, index: usize) -> &Self::Output

Performs the indexing (container[index]) operation.

impl<const E: bool> IndexMut<usize> for Vsids<E>

IndexMut trait implementation for the VSIDS variable selection strategy. Allows for mutable indexing into the scores vector.

Safety

Again, should only be used internally and with care due to the unchecked indexing.

fn index_mut(&mut self, index: usize) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl<const EARLY_EXIT: bool> PartialEq for Vsids<EARLY_EXIT>

fn eq(&self, other: &Vsids<EARLY_EXIT>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<const EARLY_EXIT: bool> PartialOrd for Vsids<EARLY_EXIT>

fn partial_cmp(&self, other: &Vsids<EARLY_EXIT>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<L: Literal, const E: bool> VariableSelection<L> for Vsids<E>

VariableSelection trait implementation for the VSIDS variable selection strategy.

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

Creates a new instance of the Vsids strategy. Initialises scores for all literals to zero and activity_inc to 1.0.

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

Picks an unassigned variable with the highest activity score by iterating through all literals.

This operation is O(N) where N is the number of variables. If EARLY_EXIT (compile-time const generic E) is true, the iteration might stop early if a literal’s score exceeds self.activity_inc * 5.0.

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

Bumps the activity scores of the specified literals. Each literal’s score is incremented by activity_inc.

fn decay(&mut self, decay: f64)

Decays the activity scores. Similar to VsidsHeap, activity_inc is divided by decay (effectively increasing it). If activity_inc exceeds VSIDS_RESCALE_THRESHOLD, all scores are rescaled by multiplying with VSIDS_RESCALE_FACTOR, and activity_inc is also set to VSIDS_RESCALE_FACTOR (note: this differs slightly from VsidsHeap which rescales activity_inc by the same factor; here it’s reset). This prevents overflow.

fn decisions(&self) -> usize

Returns the total number of decisions made by this strategy instance.

impl<const EARLY_EXIT: bool> StructuralPartialEq for Vsids<EARLY_EXIT>