On Mon, Feb 11, 2008 at 5:05 PM, Don Stewart
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.
Have you thought about uploading it to hackage.haskell.org? We've got some similar stuff up there already,
I have just done so. The package is available here: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/sat-micro-hs-0.1 -- Denis