A complete (in the logical sense) SAT solver with non-chronological backtracking. This is a Haskell implementation of (most of) the minimal OCaml solver described in the paper SAT-MICRO: petit mais costaud! by Sylvain Conchon, Johannes Kanig, and Stephane Lescuyer.