[Haskell-cafe] RFC: SAT solver using Cont/callCC for backtracking search

[Don Stewart]

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