Module preprocessing

The literal module provides functionality for working with literals in SAT problems. Defines traits and implementations for preprocessing SAT formulas.

Preprocessing techniques aim to simplify a CNF formula before handing it to the main SAT solver. This can significantly reduce the search space and improve solver performance. Common techniques include:

• Eliminating tautological clauses (e.g. x V !x V y).
• Eliminating pure literals (literals that only appear with one polarity).
• Eliminating subsumed clauses (e.g. if (x V y) exists, (x V y V z) is subsumed).

This module provides:

• The Preprocessor trait, defining a common interface for preprocessing steps.
• PreprocessorChain for applying multiple preprocessors in sequence.
• Implementations for several common preprocessing techniques.

Structs

PreprocessorChain

A chain of preprocessors, allowing multiple preprocessing techniques to be applied sequentially.

PureLiteralElimination

Preprocessor for Pure Literal Elimination.

SubsumptionElimination

Preprocessor for Subsumption Elimination.

TautologyElimination

Preprocessor for Tautology Elimination.

Traits

Preprocessor

Defines the interface for a CNF formula preprocessor.