Struct VsidsHeap

pub struct VsidsHeap { /* private fields */ }

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

This strategy maintains an activity score for each literal. Variables involved in recent conflicts get their scores “bumped”. Periodically, all scores “decay”. The BinaryHeap is used to efficiently find the unassigned literal with the highest activity score. This implementation aims for O(log N) pick operations on average, where N is the number of variables.

Trait Implementations

impl Clone for VsidsHeap

fn clone(&self) -> VsidsHeap

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VsidsHeap

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

Formats the value using the given formatter.

impl Index<usize> for VsidsHeap

Index trait implementation for the VSIDS heap. Allows for indexing into the scores vector using a usize that typically corresponds to Literal::index().

Safety

This implementation uses get_unchecked for performance

type Output = f64

The returned type after indexing.

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

Performs the indexing (container[index]) operation.

impl IndexMut<usize> for VsidsHeap

IndexMut trait implementation for the VSIDS heap. Allows for mutable indexing into the scores vector using a usize that typically corresponds to Literal::index().

Safety

Similar to the Index implementation, this uses get_unchecked_mut.

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

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

impl<L: Literal> VariableSelection<L> for VsidsHeap

VariableSelection trait implementation for the VSIDS heap.

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

Creates a new instance of the VsidsHeap strategy.

Initialises scores for all possible literals (2 * num_vars) to zero. The activity_inc is initialised to 1.0. The heap is populated with initial zero scores for all literals.

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

Picks an unassigned variable with the highest activity score.

It repeatedly pops from the heap until it finds a ScoreEntry whose corresponding variable is unassigned and whose score matches the current score in the scores vector (to filter out stale entries).

The complexity is typically O(log N) for heap pop, but can be higher if many stale entries need to be processed.

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

Bumps the activity scores of the specified literals.

For each literal in vars, its score is incremented by activity_inc, and the heap is updated accordingly via bump_internal.

fn decay(&mut self, decay: f64)

Decays the activity scores.

In this VSIDS implementation, scores are not directly decayed. Instead, activity_inc is divided by the decay factor (typically 0 < decay < 1, e.g. 0.95, so activity_inc effectively increases). This gives more weight to variables involved in more recent conflicts.

If activity_inc exceeds VSIDS_RESCALE_THRESHOLD, all scores and activity_inc are rescaled by multiplying with VSIDS_RESCALE_FACTOR to prevent overflow and maintain precision. This rescaling step involves rebuilding the heap, which can be an O(N) operation.

fn decisions(&self) -> usize

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