Struct Preprocessor 

pub struct Preprocessor { /* private fields */ }

Preprocessing context

Implementations

impl Preprocessor

pub fn new(num_vars: usize) -> Self

Create a new preprocessor

pub fn build_occurrences(&mut self, clauses: &ClauseDatabase)

Build occurrence lists from clause database

pub fn blocked_clause_elimination( &mut self, clauses: &mut ClauseDatabase, ) -> usize

Blocked Clause Elimination

Remove clauses that are blocked on some literal. Returns the number of clauses eliminated.

pub fn pure_literal_elimination( &mut self, clauses: &mut ClauseDatabase, ) -> usize

Pure Literal Elimination

A pure literal is one that appears only in positive or only in negative form. All clauses containing a pure literal can be satisfied and removed. Returns the number of clauses eliminated.

pub fn subsumption_elimination(&mut self, clauses: &mut ClauseDatabase) -> usize

Subsumption Elimination

A clause C subsumes clause D if C ⊆ D (every literal in C is in D). If C subsumes D, then D can be removed. Returns the number of clauses eliminated.

pub fn variable_elimination( &mut self, clauses: &mut ClauseDatabase, limit: usize, ) -> usize

Variable Elimination (Bounded Variable Elimination)

Eliminate a variable by resolving all pairs of clauses containing v and ~v, but only if the number of resulting clauses is not too large. Returns the number of variables eliminated.

pub fn failed_literal_probing(&mut self, clauses: &mut ClauseDatabase) -> usize

Failed Literal Probing

Try to assign each literal and propagate. If a literal leads to a conflict, we can infer its negation must be true (failed literal). Returns the number of failed literals found.

pub fn bounded_variable_addition( &mut self, clauses: &mut ClauseDatabase, max_vars_to_add: usize, ) -> usize

Bounded Variable Addition (BVA)

Introduce new variables to simplify formulas by factoring out common literals. For example, if we have clauses (a ∨ b ∨ c) and (a ∨ b ∨ d), we can replace them with: (a ∨ b ∨ x), (~x ∨ c), (~x ∨ d) where x is a fresh variable. This can reduce total clause size and improve solving.

Returns the number of variables added.

pub fn preprocess(&mut self, clauses: &mut ClauseDatabase) -> (usize, usize)

Apply all preprocessing techniques

Returns (clauses_eliminated, vars_eliminated)

Trait Implementations

impl Debug for Preprocessor

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

Formats the value using the given formatter.