This is a Programming Project that Prof. Vijay Ganesh and I designed for the course Methods and Tools for Software Engineering (ECE650 Fall2022, UWaterloo). The project asks the students to build a SAT solver in C++. The project consists of three parts:
(1) Build a parser that parses Boolean formulas. (2) Build a Boolean evaluator that evaluates the satisfiability of a formula under an assignment.
Implement Tseitin Transoformation that transforms a Boolean formula into an equisatisfiable formula in CNF.
Implement a DPLL/CDCL SAT solver.
The detailed assignment requirements, skeleton/testing codes, makefiles, and sample executables are provided in the respective folder (the Bonus description is included in PA2). Contact me if you need my complete code (the ones used to compile the sample executables) for teaching/learning purposes. Have fun coding!