sat_solver::sat::preprocessing

Trait Preprocessor

Source 
pub trait Preprocessor<L: Literal, S: LiteralStorage<L>> {
    // Required method
    fn preprocess(&self, cnf: &[Clause<L, S>]) -> Vec<Clause<L, S>>;
}
Expand description

Defines the interface for a CNF formula preprocessor.

A preprocessor takes a list of clauses (representing a CNF formula) and returns a new list of clauses, presumably simplified or transformed in a way that preserves satisfiability.

§Type Parameters

  • L: The Literal type used in clauses.
  • S: The LiteralStorage type for clauses.

Required Methods§

Source

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

Applies the preprocessing technique to the given CNF formula.

§Arguments
  • cnf: A slice of Clause<L, S> representing the input formula.
§Returns

A Vec<Clause<L, S>> representing the preprocessed formula. This new vector might contain fewer clauses, modified clauses, or new clauses.

Implementors§