wrote a small SAT solver in Haskell based on CDCL and two-watched-literal scheme.