LemmaSAT

This is a SAT solver that uses the CDCL algorithm to solve the Boolean Satisfiability Problem on CNF formulas.

Table of Contents

• To do
• Building
• Running
• References
• LICENSE
• Contributing

To do

• DIMACS Parser
• Clause Database
• Preprocessing (BCP, Pure Literal Elimination, Subsumption & SSR, Strengthening, Blocked Clause Elimination, Variable Elimination, Probing)
• CDCL Engine (Decision Heuristics, Conflict Analysis, Learning Clauses, Backtracking)
• Proof System (DRUP, LRAT and DRAT-proof)
• Policy Layer ??
• Parallelization / HPC [optional]

Building

cmake -B build -S .
cmake --build build --config Release

Running

./build/Solver/SAT-solver <path_to_dimacs_file>

References

• Unit Propagation
• CDCL
• Impact of BVE on Solving Pigeonhole Formulas
• Preprocessing in SAT Solving (if link is unreachable, DOI: 10.3233/FAIA200992)
• Kissat and CaDiCaL source codes

LICENSE

This project is licensed under the MIT License - see the LICENSE file for details.

Contributing

Contributions are not welcome. This is a personal project.