A tiny proof producing SAT solver.
- Parse DIMACS.
- Implement brute force.
- Implement DPLL.
- Tests
- Add more tests. Also will need tests for unsat results.
- Produce proofs in the brute force search.
- Produce proofs in DPLL.
- Add more algorithms. Ideas: BDD, CDCL.
- Conversion to CNF.
- Perhaps a little web interface to input formulas, to learn something about web programming
- [HOLD] (See Note.md) Create a functor to parametrize algo modules by the input format.