Towards a SAT solver written in Ltac There's no practical use for this. The point of this project is to learn how SAT solvers work by relating SAT solver proof states to Coq goals.