Struct Cnf 

pub struct Cnf<L: Literal = PackedLiteral, S: LiteralStorage<L> = SmallVec<[L; 8]>> {
    pub clauses: Vec<Clause<L, S>>,
    pub num_vars: usize,
    pub vars: Vec<Variable>,
    pub lits: Vec<L>,
    pub non_learnt_idx: usize,
}

Represents a boolean formula in Conjunctive Normal Form (CNF).

A CNF formula is a collection of clauses. The formula is satisfied if and only if all its clauses are satisfied.

Type Parameters

• L: The type of Literal used in the clauses. Defaults to PackedLiteral.
• S: The LiteralStorage type used within each Clause. Defaults to SmallVec<[L; 8]>.

Fields

clauses: Vec<Clause<L, S>>

The list of clauses that make up the CNF formula.

num_vars: usize

The highest variable identifier encountered in the formula, plus one. This represents the number of distinct variables if they are numbered contiguously from 0 or 1. If variables are 1-indexed v1, ..., vn, num_vars would be n+1. If variables are 0-indexed v0, ..., v(n-1), num_vars would be n.

vars: Vec<Variable>

A flat list of all variable identifiers present in the formula. May contain duplicates.

lits: Vec<L>

A flat list of all literals present across all clauses. May contain duplicates.

non_learnt_idx: usize

The index in clauses vector that separates original problem clauses from learnt clauses. Clauses from 0 to non_learnt_idx - 1 are original. Clauses from non_learnt_idx onwards are learnt during solving. When a Cnf is first created from a problem, non_learnt_idx is equal to clauses.len().

Implementations

impl<T: Literal, S: LiteralStorage<T>> Cnf<T, S>

pub fn new<J: IntoIterator<Item = i32>, I: IntoIterator<Item = J>>( clauses_iter: I, ) -> Self

Creates a new Cnf instance from an iterator of clauses, where each clause is itself an iterator of i32 (DIMACS literals).

Example: Cnf::new(vec![vec![1, -2], vec![2, 3]]) creates a CNF for (x1 OR !x2) AND (x2 OR x3).

During construction, it determines num_vars based on the maximum variable ID encountered. vars and lits collect all variables and literals. non_learnt_idx is set to the total number of initial clauses.

Type Parameters for Arguments

• J: An iterator yielding i32 (DIMACS literals for a single clause).
• I: An iterator yielding J (an iterator of clauses).

pub fn remove(&mut self, idx: usize)

Removes a clause at the specified index.

Arguments

• idx: The index of the clause to remove.

Panics

Panics if idx is out of bounds.

pub fn iter(&self) -> impl Iterator<Item = &Clause<T, S>>

Returns an iterator over the clauses in the CNF.

pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut Clause<T, S>>

Returns a mutable iterator over the clauses in the CNF.

pub fn add_clause(&mut self, clause: Clause<T, S>)

Adds a new clause to the CNF.

The clause is added to the end of the clauses list. If it’s considered a learnt clause, it should be added after non_learnt_idx. This function implicitly adds it as if it’s a new problem clause if non_learnt_idx isn’t managed externally before calling this for learnt clauses.

Updates num_vars, vars, and lits based on the new clause.

Arguments

• clause: The Clause<T, S> to add.

pub fn add_clause_vec(&mut self, clause_dimacs: Vec<i32>)

Adds a new clause specified as a Vec<i32> (DIMACS literals).

Converts clause_dimacs to a Clause<T, S> and then calls add_clause.

Arguments

• clause_dimacs: A vector of i32 representing the clause.

pub const fn len(&self) -> usize

Returns the total number of clauses in the CNF (both original and learnt).

pub const fn is_empty(&self) -> bool

Returns true if the CNF contains no clauses.

pub fn verify(&self, solutions: &Solutions) -> bool

Verifies if a given set of solutions satisfies the CNF formula.

A CNF is satisfied if every clause in it is satisfied. A clause is satisfied if at least one of its literals is true under the given assignment.

Arguments

• solutions: A Solutions object providing the truth assignment for variables. Solutions handles DIMACS-style variable IDs (1-indexed, signed).

Returns

true if solutions satisfies all clauses in the CNF, false otherwise.

pub fn convert<TargetL: Literal, TargetS: LiteralStorage<TargetL>>( &self, ) -> Cnf<TargetL, TargetS>

Converts this Cnf<T, S> into a Cnf<L, U> with different literal or storage types.

Each clause is converted using Clause::convert. Metadata like num_vars, vars, lits, and non_learnt_idx are also transformed or cloned.

Type Parameters

• L: The target Literal type for the new CNF.
• U: The target LiteralStorage<L> type for clauses in the new CNF.

Returns

A new Cnf<L, U> instance.

Trait Implementations

impl<L: Clone + Literal, S: Clone + LiteralStorage<L>> Clone for Cnf<L, S>

fn clone(&self) -> Cnf<L, S>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<L: Debug + Literal, S: Debug + LiteralStorage<L>> Debug for Cnf<L, S>

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

Formats the value using the given formatter.

impl<L: Default + Literal, S: Default + LiteralStorage<L>> Default for Cnf<L, S>

fn default() -> Cnf<L, S>

Returns the “default value” for a type.

impl<L: Literal, S: LiteralStorage<L>> Display for Cnf<L, S>

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

Formats the CNF into DIMACS CNF format.

Example output:

c Generated by CNF
p cnf <num_vars> <num_clauses>
1 -2 0
2 3 0

impl<T: Literal, S: LiteralStorage<T>> From<Expr> for Cnf<T, S>

fn from(expr: Expr) -> Self

Converts an Expr into a Cnf<T, S>. This is a convenience wrapper around to_cnf.

impl<L: Literal, S: LiteralStorage<L>> From<Vec<Clause<L, S>>> for Cnf<L, S>

fn from(clauses: Vec<Clause<L, S>>) -> Self

Converts a Vec<Clause<L, S>> directly into a Cnf<L, S>. Uses from_iter for consistent initialisation.

impl<L: Literal, S: LiteralStorage<L>> From<Vec<Vec<i32>>> for Cnf<L, S>

fn from(value: Vec<Vec<i32>>) -> Self

Converts Vec<Vec<i32>> (DIMACS clauses) into a Cnf<L, S>. Uses Cnf::new for construction.

impl<L: Literal, S: LiteralStorage<L>> FromIterator<Clause<L, S>> for Cnf<L, S>

fn from_iter<IterClauses: IntoIterator<Item = Clause<L, S>>>( iter: IterClauses, ) -> Self

Creates a Cnf from an iterator of Clause<L, S>.

Each clause from the iterator is added using self.add_clause. This initialises a default Cnf and then populates it. non_learnt_idx will be implicitly managed by add_clause if it updates it, or will remain 0 if add_clause only appends to clauses. A more robust way would be to collect clauses, then initialise Cnf fields properly.

impl<L: Hash + Literal, S: Hash + LiteralStorage<L>> Hash for Cnf<L, S>

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<T: Literal, S: LiteralStorage<T>> Index<usize> for Cnf<T, S>

fn index(&self, index: usize) -> &Self::Output

Accesses the clause at the given index.

Panics

Panics if index is out of bounds.

Safety

This implementation uses get_unchecked for performance

type Output = Clause<T, S>

The returned type after indexing.

impl<T: Literal, S: LiteralStorage<T>> IndexMut<usize> for Cnf<T, S>

fn index_mut(&mut self, index: usize) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl<L: Ord + Literal, S: Ord + LiteralStorage<L>> Ord for Cnf<L, S>

fn cmp(&self, other: &Cnf<L, S>) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl<L: PartialEq + Literal, S: PartialEq + LiteralStorage<L>> PartialEq for Cnf<L, S>

fn eq(&self, other: &Cnf<L, S>) -> 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<L: PartialOrd + Literal, S: PartialOrd + LiteralStorage<L>> PartialOrd for Cnf<L, S>

fn partial_cmp(&self, other: &Cnf<L, S>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<T: Literal, S: LiteralStorage<T>> TryFrom<Cnf<T, S>> for Expr

fn try_from(cnf: Cnf<T, S>) -> Result<Self, Self::Error>

Attempts to convert a Cnf<T, S> back into an Expr. The resulting Expr will be a conjunction of disjunctions. Returns an error if the CNF is empty (contains no clauses).

type Error = &'static str

The type returned in the event of a conversion error.

impl<L: Eq + Literal, S: Eq + LiteralStorage<L>> Eq for Cnf<L, S>

impl<L: Literal, S: LiteralStorage<L>> StructuralPartialEq for Cnf<L, S>