Struct PureLiteralElimination

pub struct PureLiteralElimination;

Preprocessor for Pure Literal Elimination.

A pure literal is a literal that appears in the formula with only one polarity (e.g. x appears but !x does not, or vice versa). If a literal l is pure:

• All clauses containing l can be satisfied by setting l to true. These clauses can be removed.
• Literals that are pure do not need to be part of the simplified formula sent to the solver, as their assignment is determined.

This implementation removes clauses containing any pure literal.

Implementations

impl PureLiteralElimination

pub fn find_pures<L: Literal, S: LiteralStorage<L>>( cnf: &[Clause<L, S>], ) -> FxHashSet<L>

Finds all pure literals in the given CNF formula.

A literal l is pure if its negation !l does not appear in any clause while l itself does appear.

The complexity is roughly proportional to the total number of literals in the CNF.

Arguments

• cnf: A slice of Clause<L, S>.

Returns

A FxHashSet<L> containing all pure literals found.

Trait Implementations

impl Clone for PureLiteralElimination

fn clone(&self) -> PureLiteralElimination

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PureLiteralElimination

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

Formats the value using the given formatter.

impl Default for PureLiteralElimination

fn default() -> PureLiteralElimination

Returns the “default value” for a type.

impl PartialEq for PureLiteralElimination

fn eq(&self, other: &PureLiteralElimination) -> 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 PureLiteralElimination

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

Applies pure literal elimination.

1. Finds all pure literals in the cnf.
2. Removes all clauses that contain any of these pure literals. (Assigning a pure literal l to true satisfies any clause containing l.)

The complexity is dominated by find_pures and iterating through clauses again.

impl Copy for PureLiteralElimination

impl Eq for PureLiteralElimination

impl StructuralPartialEq for PureLiteralElimination