Enum SATResult 

pub enum SATResult {
    Satisfiable(Vec<i32>),
    Unsatisfiable,
    Unknown,
}

The result of a SAT solver execution.

A SAT problem can have three possible outcomes:

• Satisfiable: A satisfying assignment exists
• Unsatisfiable: No satisfying assignment exists
• Unknown: The solver couldn’t determine satisfiability (e.g., due to timeout or resource limits)

Example

use sat_solvers::SATResult;

let result = SATResult::Satisfiable(vec![1, -2, 3]);

if result.is_satisfiable() {
    if let SATResult::Satisfiable(assignment) = result {
        // assignment contains the satisfying variable assignments
        // Positive values mean the variable is true, negative means false
        assert!(assignment.contains(&1));  // x1 = true
        assert!(assignment.contains(&-2)); // x2 = false
    }
}

Variants

Satisfiable(Vec<i32>)

The formula is satisfiable. Contains the satisfying assignment as a vector of literals. Positive values indicate the variable is true, negative values indicate the variable is false.

Unsatisfiable

The formula is unsatisfiable (no satisfying assignment exists).

Unknown

The solver could not determine satisfiability (e.g., timeout).

Implementations

impl SATResult

pub fn is_satisfiable(&self) -> bool

Returns true if the result is Satisfiable.

Example

use sat_solvers::SATResult;

let sat = SATResult::Satisfiable(vec![1, -2]);
let unsat = SATResult::Unsatisfiable;

assert!(sat.is_satisfiable());
assert!(!unsat.is_satisfiable());

pub fn is_unsatisfiable(&self) -> bool

Returns true if the result is Unsatisfiable.

Example

use sat_solvers::SATResult;

let unsat = SATResult::Unsatisfiable;
assert!(unsat.is_unsatisfiable());

pub fn is_unknown(&self) -> bool

Returns true if the result is Unknown.

Example

use sat_solvers::SATResult;

let unknown = SATResult::Unknown;
assert!(unknown.is_unknown());

Trait Implementations

impl Clone for SATResult

fn clone(&self) -> SATResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SATResult

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

Formats the value using the given formatter.

impl Display for SATResult

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

Formats the value using the given formatter.

impl PartialEq for SATResult

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

impl StructuralPartialEq for SATResult