Struct Solutions

pub struct Solutions {
    pub assignments: FxHashSet<NonZeroI32>,
}

Represents a satisfying assignment (a model) for a CNF formula.

The assignments are stored as a set of NonZeroI32, where:

• A positive integer v means variable v is assigned true.
• A negative integer -v means variable v is assigned false. This aligns with the DIMACS convention for representing literals.

Fields

assignments: FxHashSet<NonZeroI32>

A set of non-zero integers representing the truth assignments of variables. Positive v means variable v is true; negative -v means variable v is false.

Implementations

impl Solutions

pub fn new(s: &[i32]) -> Self

Creates a new Solutions instance from a slice of i32 (DIMACS literals). Zero values in the input slice are ignored, as NonZeroI32 cannot be zero.

pub fn iter(&self) -> impl Iterator<Item = &NonZeroI32>

Returns an iterator over the assigned literals (&NonZeroI32).

pub fn check(&self, i: NonZeroI32) -> bool

Checks if a given literal (represented by NonZeroI32) is part of the solution. For example, check(NonZeroI32::new(1).unwrap()) checks if variable 1 is true. check(NonZeroI32::new(-2).unwrap()) checks if variable 2 is false.

pub fn len(&self) -> usize

Returns the number of variables assigned in this solution.

pub fn is_empty(&self) -> bool

Returns true if this solution assigns no variables.

pub fn add(&mut self, i: NonZeroI32)

Adds a literal assignment to the solution set.

Trait Implementations

impl Clone for Solutions

fn clone(&self) -> Solutions

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Solutions

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

Formats the value using the given formatter.

impl Default for Solutions

fn default() -> Solutions

Returns the “default value” for a type.

impl Display for Solutions

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

Formats the solution as a space-separated string of assigned literals. For example: “1 -2 3” means x1=true, x2=false, x3=true.

impl PartialEq for Solutions

fn eq(&self, other: &Solutions) -> 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 Eq for Solutions

impl StructuralPartialEq for Solutions