Trait Assignment

Source

pub trait Assignment:
    Index<usize, Output = VarState>
    + IndexMut<usize, Output = VarState>
    + Debug
    + Clone {
    // Required methods
    fn new(n_vars: usize) -> Self;
    fn num_vars(&self) -> usize;
    fn set(&mut self, var: Variable, b: bool);
    fn reset(&mut self);
    fn unassign(&mut self, var: Variable);
    fn get_solutions(&self) -> Solutions;
    fn all_assigned(&self) -> bool;

    // Provided methods
    fn assign(&mut self, l: impl Literal) { ... }
    fn is_assigned(&self, var: Variable) -> bool { ... }
    fn var_value(&self, var: Variable) -> Option<bool> { ... }
    fn literal_value(&self, l: impl Literal) -> Option<bool> { ... }
    fn unassigned(&self) -> impl Iterator<Item = Variable> + '_ { ... }
}

Expand description

Trait defining the interface for managing variable assignments.

This trait allows for different underlying data structures (e.g. Vec, HashMap) to store and manage the states of variables in a SAT solver. Variables are typically represented by usize indices for direct access, or Variable (a u32 alias) for semantic clarity. Assumes 0-indexed variables if Variable is a numeric type used as an index.

Required Methods§

Source

fn new(n_vars: usize) -> Self

Creates a new assignment manager for n_vars variables.

All variables are initially Unassigned.

§Arguments

n_vars: The total number of variables to manage.

Source

fn num_vars(&self) -> usize

Returns the total number of variables this assignment manager is configured for.

Source

fn set(&mut self, var: Variable, b: bool)

Sets the truth value of a variable.

§Arguments

var: The variable to assign.
b: The boolean value to assign (true or false).

Source

fn reset(&mut self)

Resets all variables to the Unassigned state.

Source

fn unassign(&mut self, var: Variable)

Sets a variable to the Unassigned state.

§Arguments

var: The variable to unassign.

Source

fn get_solutions(&self) -> Solutions

Retrieves the current set of assigned variables as a Solutions object.

Solutions expects 1-indexed variable IDs for DIMACS compatibility.

Source

fn all_assigned(&self) -> bool

Checks if all variables managed by this assignment are currently assigned.

§Returns

true if all variables have a truth value, false otherwise.

Provided Methods§

Source

fn assign(&mut self, l: impl Literal)

Assigns a truth value to a variable based on a literal.

The variable of the literal is assigned the literal’s polarity. For example, if l is x_i, x_i is set to true. If l is !x_i, x_i is set to false.