dbueno:
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.
Have you thought about uploading it to hackage.haskell.org? We've got some similar stuff up there already, http://hackage.haskell.org/cgi-bin/hackage-scripts/package/sat-1.1.1 so feel free to upload this code! -- Don