A set of Boolean logic functions and SAT solvers looking at propositional logic and satisfiability.
- Pure Literal Eliminator: Simplifies formulas by removing pure literals.
- DIMACS Converter: Parses standard DIMACS CNF files.
- Simple SAT Solver: Uses basic variable selection rules to search for solutions.
- Unit Propagator: Applies unit clause propagation to simplify formulas.
- Branching SAT Solver: Recursively explores variable assignments.
- DPLL Solver: Implements the classic DPLL algorithm combining unit propagation, PL elimination, and recursive backtracking.