TinySAT

A tiny proof producing SAT solver.

Road map:

• 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.