Struct KSatisfiability 

pub struct KSatisfiability<K: KValue> { /* 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. This is the decision version of the problem.

Type Parameters

• K - A type implementing KValue that specifies the number of literals per clause

Example

use problemreductions::models::formula::{KSatisfiability, CNFClause};
use problemreductions::variant::K3;
use problemreductions::{Problem, Solver, BruteForce};

// 3-SAT formula: (x1 OR x2 OR x3) AND (NOT x1 OR x2 OR NOT x3)
let problem = KSatisfiability::<K3>::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_all_satisfying(&problem);
assert!(!solutions.is_empty());

Implementations

impl<K: KValue> KSatisfiability<K>

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

Create a new K-SAT problem.

Panics

Panics if any clause does not have exactly K literals (when K is a concrete value like K2, K3). When K is KN (arbitrary), no clause-length validation is performed.

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

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 (when K is a concrete value like K2, K3). When K is KN (arbitrary), no clause-length validation is performed.

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 num_literals(&self) -> usize

Get the total number of literals across all clauses.

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<K: Clone + KValue> Clone for KSatisfiability<K>

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

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<K: Debug + KValue> Debug for KSatisfiability<K>

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

Formats the value using the given formatter.

impl<'de, K: KValue> Deserialize<'de> for KSatisfiability<K>

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl<K: KValue> Problem for KSatisfiability<K>

const NAME: &'static str = "KSatisfiability"

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

type Metric = bool

The evaluation metric type.

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

Configuration space dimensions. Each entry is the cardinality of that variable.

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

Evaluate the problem on a configuration.

fn variant() -> Vec<(&'static str, &'static str)>

Returns variant attributes derived from type parameters.

fn num_variables(&self) -> usize

Number of variables (derived from dims).

impl ReduceTo<KSatisfiability<K3>> for Satisfiability

type Result = ReductionSATToKSAT<K3>

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<KSatisfiability<KN>> for KSatisfiability<K2>

type Result = ReductionAutoCast<KSatisfiability<K2>, KSatisfiability<KN>>

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<KSatisfiability<KN>> for KSatisfiability<K3>

type Result = ReductionAutoCast<KSatisfiability<K3>, KSatisfiability<KN>>

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<QUBO> for KSatisfiability<K2>

type Result = ReductionKSatToQUBO

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<QUBO> for KSatisfiability<K3>

type Result = Reduction3SATToQUBO

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<Satisfiability> for KSatisfiability<K2>

type Result = ReductionKSATToSAT<K2>

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<Satisfiability> for KSatisfiability<K3>

type Result = ReductionKSATToSAT<K3>

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<Satisfiability> for KSatisfiability<KN>

type Result = ReductionKSATToSAT<KN>

The reduction result type.

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

Reduce this problem to the target problem type.

impl ReduceTo<SubsetSum> for KSatisfiability<K3>

type Result = Reduction3SATToSubsetSum

The reduction result type.

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

Reduce this problem to the target problem type.

impl<K: KValue> Serialize for KSatisfiability<K>

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl DeclaredVariant for KSatisfiability<K2>

impl DeclaredVariant for KSatisfiability<K3>

impl DeclaredVariant for KSatisfiability<KN>

impl<K: KValue> SatisfactionProblem for KSatisfiability<K>