Struct Satisfiability 

pub struct Satisfiability<W = i32> { /* private fields */ }

Boolean Satisfiability (SAT) problem in CNF form.

Given a Boolean formula in conjunctive normal form (CNF), determine if there exists an assignment that satisfies all clauses.

The problem can be weighted, where the goal is to maximize the total weight of satisfied clauses (MAX-SAT).

Example

use problemreductions::models::satisfiability::{Satisfiability, CNFClause};
use problemreductions::{Problem, Solver, BruteForce};

// Formula: (x1 OR x2) AND (NOT x1 OR x3) AND (NOT x2 OR NOT x3)
let problem = Satisfiability::<i32>::new(
    3,
    vec![
        CNFClause::new(vec![1, 2]),      // x1 OR x2
        CNFClause::new(vec![-1, 3]),     // NOT x1 OR x3
        CNFClause::new(vec![-2, -3]),    // NOT x2 OR NOT x3
    ],
);

let solver = BruteForce::new();
let solutions = solver.find_best(&problem);

// Verify solutions satisfy all clauses
for sol in solutions {
    assert!(problem.solution_size(&sol).is_valid);
}

Implementations

impl<W: Clone + Default> Satisfiability<W>

pub fn new(num_vars: usize, clauses: Vec<CNFClause>) -> Self

where W: From<i32>,

Create a new SAT problem with unit weights.

pub fn with_weights( num_vars: usize, clauses: Vec<CNFClause>, weights: Vec<W>, ) -> Self

Create a new weighted SAT problem (MAX-SAT).

pub fn num_vars(&self) -> usize

Get the number of variables.

pub fn num_clauses(&self) -> usize

Get the number of clauses.

pub fn clauses(&self) -> &[CNFClause]

Get the clauses.

pub fn get_clause(&self, index: usize) -> Option<&CNFClause>

Get a specific clause.

pub fn count_satisfied(&self, assignment: &[bool]) -> usize

Count satisfied clauses for an assignment.

pub fn is_satisfying(&self, assignment: &[bool]) -> bool

Check if an assignment satisfies all clauses.

Trait Implementations

impl<W: Clone> Clone for Satisfiability<W>

fn clone(&self) -> Satisfiability<W>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<W> ConstraintSatisfactionProblem for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + 'static,

fn constraints(&self) -> Vec<LocalConstraint>

Returns the hard constraints that must be satisfied.

fn objectives(&self) -> Vec<LocalSolutionSize<Self::Size>>

Returns the local objectives that contribute to solution size.

fn weights(&self) -> Vec<Self::Size>

Returns the weights for the problem (e.g., vertex weights).

fn set_weights(&mut self, weights: Vec<Self::Size>)

Set new weights for the problem.

fn is_weighted(&self) -> bool

Returns whether the problem has non-uniform weights.

fn is_satisfied(&self, config: &[usize]) -> bool

Check if all constraints are satisfied by a configuration.

fn compute_objective(&self, config: &[usize]) -> Self::Size

Compute the total objective value from all local objectives.

impl<W: Debug> Debug for Satisfiability<W>

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

Formats the value using the given formatter.

impl<'de, W> Deserialize<'de> for Satisfiability<W>

where W: Deserialize<'de>,

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<W> Problem for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + 'static,

const NAME: &'static str = "Satisfiability"

Base name of this problem type (e.g., “IndependentSet”).

type GraphType = SimpleGraph

The graph type this problem operates on.

type Weight = W

The weight type for this problem.

type Size = W

The type used for objective/size values.

fn num_variables(&self) -> usize

Returns the number of variables in the problem.

fn num_flavors(&self) -> usize

Returns the number of possible values (flavors) for each variable. For binary problems, this is 2.

fn problem_size(&self) -> ProblemSize

Returns metadata about the problem size.

fn energy_mode(&self) -> EnergyMode

Returns whether larger or smaller objective values are better.

fn solution_size(&self, config: &[usize]) -> SolutionSize<Self::Size>

Evaluate the solution size for a given configuration.

fn variables(&self) -> Range<usize>

Returns the range of variable indices.

fn flavors(&self) -> Vec<usize>

Returns the possible flavors as a vector.

fn is_valid_config(&self, config: &[usize]) -> bool

Check if a configuration is valid for this problem.

fn solution_size_multiple( &self, configs: &[Vec<usize>], ) -> Vec<SolutionSize<Self::Size>>

Evaluate multiple configurations at once (batch evaluation).

impl<W> ReduceTo<Coloring> for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionSATToColoring<W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<W> ReduceTo<DominatingSet<W>> for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionSATToDS<W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<W> ReduceTo<IndependentSet<W>> for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionSATToIS<W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<W> ReduceTo<KSatisfiability<3, W>> for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionSATToKSAT<3, W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<W> ReduceTo<KSatisfiability<4, W>> for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionSATToKSAT<4, W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<W> ReduceTo<KSatisfiability<5, W>> for Satisfiability<W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionSATToKSAT<5, W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<const K: usize, W> ReduceTo<Satisfiability<W>> for KSatisfiability<K, W>

where W: Clone + Default + PartialOrd + Num + Zero + AddAssign + From<i32> + 'static,

type Result = ReductionKSATToSAT<K, W>

The reduction result type.

fn reduce_to(&self) -> Self::Result

Reduce this problem to the target problem type.

impl<W> Serialize for Satisfiability<W>

where W: Serialize,

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.