- None; almost have a basic sat solver working. It works for some cases (e.g. f008-01-s.cnf and f008-01-u.cnf) but not others (e.g. f008-02-s.cnf) and we haven't finished debugging it to figure out why some becnhmarks don't work.
- System requirements: built and tested on MacOS Monterey, compiled using g++ or clang++ in
compile.sh - To compile:
./compile.sh - To run:
./sat-solver \[limit\] \[input cnf file\] \[output sat file\]
- Wrote readInput() and writeOutput()
- Debugging
- Wrote DPLL() and associated functions
- Debugging
This is a boolean satisfiability solver written for a graduate-level algorithms and modeling course. It takes input in conjunctive normative form (CNF) and provides outputs in a file specifying satisfiability and values which satisfy the input if it is satisfiable.