Struct Clause

pub struct Clause<L: Literal = PackedLiteral, S: LiteralStorage<L> = SmallVec<[L; 8]>> {
    pub literals: S,
    pub lbd: u32,
    pub deleted: bool,
    pub is_learnt: bool,
    pub activity: OrderedFloat<f64>,
    /* private fields */
}

Represents a clause in a SAT formula.

A clause is a set of literals, typically interpreted as a disjunction. For example, the clause {L1, L2, L3} represents L1 OR L2 OR L3.

Type Parameters

• L: The type of literal stored in the clause. Defaults to PackedLiteral. Must implement the Literal trait.
• S: The storage type for the literals. Defaults to SmallVec<[L; 8]>. Must implement the LiteralStorage<L> trait, providing storage for literals.

Fields

literals: S

The collection of literals forming the clause. The specific storage (e.g. Vec, SmallVec) is determined by the S type parameter.

lbd: u32

Literal Blocks Distance (LBD) of the clause. LBD is a measure of the “locality” of a learnt clause in terms of decision levels. Lower LBD often indicates higher quality learnt clauses. Calculated for learnt clauses.

deleted: bool

Flag indicating if the clause has been marked for deletion. Deleted clauses are removed by the solver during database cleaning.

is_learnt: bool

Flag indicating if the clause was learnt during conflict analysis. Original clauses (from the input problem) are not marked as learnt.

activity: OrderedFloat<f64>

Activity score of the clause, used in clause deletion heuristics (e.g. VSIDS-like). Higher activity suggests the clause has been more recently involved in conflicts or propagations.

Implementations

impl<L: Literal, S: LiteralStorage<L>> Clause<L, S>

pub fn new(literals_slice: &[L]) -> Self

Creates a new clause from a slice of literals.

Arguments

• literals_slice: A slice of literals to form the clause.

pub fn resolve(&self, other: &Self, pivot: L) -> Self

Performs resolution between this clause and another clause on a pivot literal.

The resolution rule is: (A V x) AND (B V !x) => (A V B). In this context, self represents (A V x) and other represents (B V !x). The pivot argument is the literal x.

• If pivot (i.e. x) is not found in self.literals, or pivot.negated() (i.e. !x) is not found in other.literals, resolution is not applicable with the given pivot. In this case, a clone of self is returned.
• The resolvent clause is formed by taking the union of literals from self (excluding pivot) and other (excluding pivot.negated()), with duplicates removed.
• If the resulting resolvent is a tautology (e.g. contains both y and !y), a default (typically empty and non-learnt) clause is returned. A tautological resolvent is logically true and provides no new constraints.

Arguments

• other: The other clause to resolve with.
• pivot: The literal x to resolve upon. self should contain pivot, and other should contain pivot.negated().

Returns

The resolved clause. This is a new Clause instance.

pub fn resolve_binary(&self, binary: &Self) -> Option<Self>

Performs binary resolution: resolves self with a binary clause binary.

A binary clause contains exactly two literals. Let binary be (L1 V L2).

• If self contains !L1, the result is (self - {!L1}) V {L2}.
• If self contains !L2, the result is (self - {!L2}) V {L1}. The literals in the resulting clause are unique. If the resulting clause is a tautology, None is returned.

Arguments

• binary: A binary clause (must have exactly two literals).

Returns

Some(resolved_clause) if resolution is possible and the result is not a tautology. None if binary is not a binary clause, resolution is not applicable (no matching negated literal found), or the result of resolution is a tautology.

Panics

The unwrap_or_else for position might lead to unexpected behavior if the literal to be removed is not found (which shouldn’t happen if lit was found in self.literals and new_clause is a clone). If position returns None, remove_literal would attempt to remove the last element of new_clause.literals.

pub fn push(&mut self, literal: L)

Adds a literal to the clause, if it is not already present.

Arguments

• literal: The literal to add.

pub fn is_tautology(&self) -> bool

Checks if the clause is a tautology.

A clause is a tautology if it contains both a literal and its negation (e.g. x OR !x). Such clauses are always true and not useful

Returns

true if the clause is a tautology, false otherwise.

pub fn len(&self) -> usize

Returns the number of literals in the clause.

pub fn iter(&self) -> impl Iterator<Item = &L>

Returns an iterator over the literals in the clause.

pub fn iter_mut(&mut self) -> impl Iterator<Item = &mut L>

Returns a mutable iterator over the literals in the clause.

pub fn swap(&mut self, i: usize, j: usize)

Swaps two literals in the clause by their indices.

Arguments

• i: The index of the first literal.
• j: The index of the second literal.

Panics

Panics if i or j are out of bounds for self.literals.

pub fn is_unit(&self) -> bool

Checks if the clause is a unit clause.

A unit clause is a clause with exactly one literal.

Returns

true if the clause has exactly one literal, false otherwise.

pub fn is_empty(&self) -> bool

Checks if the clause is empty.

An empty clause (containing no literals) represents a contradiction (logical false).

Returns

true if the clause has no literals, false otherwise.

pub const fn is_deleted(&self) -> bool

Checks if the clause is marked as deleted.

pub const fn delete(&mut self)

Marks the clause as deleted.

This only sets the deleted flag to true. It does not remove the clause

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

Removes a literal from the clause at the given index.

This method uses swap_remove for efficiency, which means the order of the remaining literals in the clause may change (the last literal is swapped into the idx position, and then the length is reduced).

Arguments

• idx: The index of the literal to remove.

Panics

Panics if idx is out of bounds for self.literals.

pub fn calculate_lbd(&mut self, trail: &Trail<L, S>)

Calculates and updates the Literal Block Distance (LBD) of the clause.

LBD is defined as the number of distinct decision levels (excluding level 0) of the variables in the clause’s literals. This metric is used to estimate the “quality” or “usefulness” of learnt clauses

Special LBD rules applied:

• If the clause is empty, LBD is 0.
• If all literals are at decision level 0 (or unassigned and treated as level 0), and the clause is not empty, LBD is 1.
• For learnt, non-empty clauses, LBD is ensured to be at least 1.

Arguments

• trail: The solver’s assignment trail, used to find the decision level of each literal’s variable.

Panics

Behavior of BitVec indexing with level (a u32) depends on usize size.

pub fn convert<T: Literal, U: LiteralStorage<T>>(&self) -> Clause<T, U>

Converts this clause into a clause with different literal or storage types.

This is useful for benchmarking primarily The literals are converted one by one using T::new(original_lit.variable(), original_lit.polarity()). Metadata like LBD, deleted status, learnt status, and activity are copied.

Type Parameters

• T: The target Literal type for the new clause.
• U: The target LiteralStorage<T> type for the new clause.

Returns

A new Clause<T, U> with equivalent literals and copied metadata.

pub fn bump_activity(&mut self, increment: f64)

Increases the activity score of the clause by a specified increment.

This is part of VSIDS-like (Variable State Independent Decaying Sum) heuristics, where clauses involved in recent conflict analysis get their activity “bumped”, making them less likely to be deleted.

Arguments

• increment: The positive amount to add to the clause’s activity score.

pub fn decay_activity(&mut self, factor: f64)

Decays the activity score of the clause by a multiplicative factor.

Arguments

• factor: The factor to multiply the activity score by (typically between 0 and 1).

pub const fn activity(&self) -> f64

Returns the raw floating-point activity score of the clause.

Trait Implementations

impl<L: Literal, S: LiteralStorage<L>> AsRef<[L]> for Clause<L, S>

fn as_ref(&self) -> &[L]

Returns a slice containing the literals in the clause. This allows the clause to be treated as a slice for read-only operations.

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

fn clone(&self) -> Clause<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 Clause<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 Clause<L, S>

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

Returns the “default value” for a type.

impl<T: Literal, S: LiteralStorage<T>> From<&Clause<T, S>> for Vec<T>

fn from(clause: &Clause<T, S>) -> Self

Converts a reference to a clause into a Vec of its literals.

The literals are copied from the clause’s internal storage into a new Vec<T>.

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

fn from(literals_vec: &Vec<L>) -> Self

Creates a clause from a reference to a Vec<L>, cloning the literals.

The literals from literals_vec are cloned to create the literals field.

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

fn from(literals_vec: Vec<L>) -> Self

Creates a clause directly from a Vec<L>.

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

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

Creates a clause from a Vec<i32>, where integers represent literals in DIMACS format (e.g. 1 for variable 1 true, -2 for variable 2 false).

This constructor uses Clause::new, so literals will be deduplicated. Other fields (lbd, deleted, etc.) are initialised to defaults.

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: Literal, S: LiteralStorage<L>> FromIterator<L> for Clause<L, S>

fn from_iter<I: IntoIterator<Item = L>>(iter: I) -> Self

Creates a new clause from an iterator of literals.

The literals from the iterator are collected into the literals field.

Literals are deduplicated during creation using itertools::Itertools::unique. For example, [L1, L1, L2] becomes {L1, L2}.

The clause is initialised as not learnt, not deleted, with LBD 0 and activity 0.0. Other fields (lbd, deleted, is_learnt, activity) are initialised to default values.

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

fn from_iter<I: IntoIterator<Item = i32>>(iter: I) -> Self

Creates a clause from an iterator of i32 (DIMACS literals).

This is similar to From<Vec<i32>>. Literals are converted from DIMACS format. See From<Vec<i32>> for more details on DIMACS conversion and variable indexing.

impl<L: Hash + Literal, S: Hash + LiteralStorage<L>> Hash for Clause<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 Clause<T, S>

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

Accesses the literal at the given index within the clause.

Panics

Panics if index is out of bounds for self.literals.

Safety

This implementation uses get_unchecked for performance

type Output = T

The returned type after indexing.

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

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

Mutably accesses the literal at the given index within the clause.

Panics

Panics if index is out of bounds for self.literals.

Safety

This implementation uses get_unchecked_mut for performance.

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

fn cmp(&self, other: &Clause<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 Clause<L, S>

fn eq(&self, other: &Clause<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 Clause<L, S>

fn partial_cmp(&self, other: &Clause<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<L: Eq + Literal, S: Eq + LiteralStorage<L>> Eq for Clause<L, S>

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