Enum Objective 

pub enum Objective {
    Satisfaction,
    MaxSat,
    MinUnsat,
}

The optimization objective for a SAT/MaxSAT instance.

This determines what the solver should optimize for:

• Satisfaction: Find any satisfying assignment (standard SAT)
• MaxSat: Maximize the number/weight of satisfied clauses
• MinUnsat: Minimize the number/weight of unsatisfied clauses

Variants

Satisfaction

Find any satisfying assignment (decision problem).

The solver returns SAT if an assignment exists that satisfies all clauses, or UNSAT if no such assignment exists.

MaxSat

Maximize the total weight of satisfied clauses (optimization).

For unweighted instances, this maximizes the count of satisfied clauses. The solver finds an assignment that maximizes the objective.

MinUnsat

Minimize the total weight of unsatisfied clauses (optimization).

This is equivalent to MaxSAT for complete solvers but may differ for incomplete/approximate solvers.

Trait Implementations

impl Clone for Objective

fn clone(&self) -> Objective

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Objective

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

Formats the value using the given formatter.

impl Default for Objective

fn default() -> Objective

Returns the “default value” for a type.

impl Hash for Objective

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Objective

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

impl Eq for Objective

impl StructuralPartialEq for Objective