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

[Denis Bueno]

On Mon, Feb 11, 2008 at 5:05 PM, Don Stewart <dons at galois.com> wrote:
>  > 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