Struct LearnedClause 

pub struct LearnedClause {
    pub literals: Vec<(usize, i32)>,
    pub activity: f64,
}

A learned nogood clause: a disjunction of negated literals.

A clause {(i₁, v₁), (i₂, v₂), …} is violated (and triggers pruning) when every literal matches a current decision: decision[iⱼ] == vⱼ for all j.

Fields

literals: Vec<(usize, i32)>

Literals (var_index, value). The clause fires when all literals are satisfied simultaneously by the current decision trail.

activity: f64

Activity score of this clause (used for clause deletion).

Implementations

impl LearnedClause

pub fn new(literals: Vec<(usize, i32)>) -> Self

Create a new learned clause from a slice of variable-value pairs.

pub fn len(&self) -> usize

Return the number of literals in the clause.

pub fn is_empty(&self) -> bool

Return true if the clause has no literals (tautology / empty).

pub fn subsumes(&self, other: &LearnedClause) -> bool

Check whether this clause subsumes other, i.e., every literal of self also appears in other. A subsuming clause is strictly stronger (shorter or equal).

Trait Implementations

impl Clone for LearnedClause

fn clone(&self) -> LearnedClause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LearnedClause

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

Formats the value using the given formatter.