Hi all, I've recently done a small Haskell port of some OCaml code from a paper entitled "SAT-MICRO: petit mais costaud!" It's a tiny (one emacs buffer for the algorithm, ~160 lines overall) DPLL SAT solver with non-chronological backtracking, implemented using the Cont monad and callCC. If anyone has time and interest, I'm requesting comments on how the code could be improved in any way: style, efficiency, etc. The code in the paper is OCaml which uses exceptions as the main control-flow mechanism for backtracking. If you can read French, you may be interested in the paper, which is available here: http://hal.inria.fr/inria-00202831/en/ Of course, you will likely understand the OCaml code even if you don't understand French. Thanks in advance to anyone who comments. -- Denis