Struct KSatisfiability 

pub struct KSatisfiability<const K: usize, W = i32> { /* private fields */ }

K-Satisfiability problem where each clause has exactly K literals.

This is a restricted form of SAT where every clause must contain exactly K literals. The most famous variant is 3-SAT (K=3), which is NP-complete, while 2-SAT (K=2) is solvable in polynomial time.

Type Parameters

• K - The number of literals per clause (compile-time constant)
• W - The weight type for MAX-K-SAT

Example

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

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

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

Implementations

impl<const K: usize, W: Clone + Default> KSatisfiability<K, W>

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

where W: From<i32>,

Create a new K-SAT problem with unit weights.

Panics

Panics if any clause does not have exactly K literals.

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

where W: From<i32>,

Create a new K-SAT problem allowing clauses with fewer than K literals.

This is useful when the reduction algorithm produces clauses with fewer literals (e.g., when allow_less is true in the Julia implementation).

Panics

Panics if any clause has more than K literals.

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

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

Panics

Panics if any clause does not have exactly K literals, or if the number of weights doesn’t match the number of clauses.

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<const K: usize, W: Clone> Clone for KSatisfiability<K, W>

fn clone(&self) -> KSatisfiability<K, W>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const K: usize, W> ConstraintSatisfactionProblem for KSatisfiability<K, 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<const K: usize, W: Debug> Debug for KSatisfiability<K, W>

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

Formats the value using the given formatter.

impl<'de, const K: usize, W> Deserialize<'de> for KSatisfiability<K, 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<const K: usize, W> Problem for KSatisfiability<K, W>

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

const NAME: &'static str = "KSatisfiability"

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<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<const K: usize, W> Serialize for KSatisfiability<K, 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.