Struct SubsumptionElimination

pub struct SubsumptionElimination;

Preprocessor for Subsumption Elimination.

A clause C1 subsumes another clause C2 if all literals of C1 are also present in C2 (i.e. C1 is a sub-clause of C2). If C1 subsumes C2, C2 is redundant and can be removed. For example, if (x V y) exists, then (x V y V z) is subsumed.

This implementation assumes literals within clauses are sorted for efficient checking.

Trait Implementations

impl Clone for SubsumptionElimination

fn clone(&self) -> SubsumptionElimination

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SubsumptionElimination

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

Formats the value using the given formatter.

impl Default for SubsumptionElimination

fn default() -> SubsumptionElimination

Returns the “default value” for a type.

impl PartialEq for SubsumptionElimination

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

fn preprocess(&self, cnf: &[Clause<L, S>]) -> Vec<Clause<L, S>>

Applies subsumption elimination.

Iterates through pairs of clauses. If clause C_i subsumes C_j, C_j is marked for removal. To optimise, clauses are typically sorted by length first: a shorter clause can subsume a longer one, but not vice versa.

impl Copy for SubsumptionElimination

impl Eq for SubsumptionElimination

impl StructuralPartialEq for SubsumptionElimination