Module variable_selection

The variable_selection module implements various strategies for selecting variables during the solving process. Defines variable selection strategies (decision heuristics) for SAT solvers.

The variable selection strategy (often called the decision heuristic) determines which unassigned variable to pick next and what truth value to assign to it during the search process. A good heuristic can significantly impact solver performance.

This module provides:

• The VariableSelection trait, defining a common interface for these strategies.
• Several concrete implementations:
  • VsidsHeap: Implements VSIDS (Variable State Independent Decaying Sum) using a binary heap to efficiently find the variable with the highest activity score.
  • Vsids: A simpler VSIDS implementation that iterates through scores without a heap.
  • FixedOrder: Selects variables in a fixed, predefined order (e.g. by variable index).
  • RandomOrder: Selects variables in a (shuffled) random order.
  • JeroslowWangOneSided: Implements the Jeroslow-Wang heuristic (one-sided version), which scores literals based on their occurrence in short clauses.
  • JeroslowWangTwoSided: A two-sided version of the Jeroslow-Wang heuristic.

Structs

FixedOrder

A variable selection strategy that picks variables in a fixed, predefined order.

JeroslowWangOneSided

Implements the Jeroslow-Wang heuristic (one-sided version).

JeroslowWangTwoSided

Implements a two-sided version of the Jeroslow-Wang heuristic.

RandomOrder

A variable selection strategy that picks variables in a random order.

Vsids

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

VsidsHeap

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

Enums

VariableSelectionImpls

Enum to encapsulate different variable selection implementations.

VariableSelectionType

Enum representing different variable selection strategies.

Constants

VSIDS_DECAY_FACTOR

A constant for the decay factor used in VSIDS-like heuristics.

Traits

VariableSelection

Trait defining the interface for variable selection strategies.