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

Don Stewart dons at galois.com
Mon Feb 11 17:05:51 EST 2008

> 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,


so feel free to upload this code!

-- Don

More information about the Haskell-Cafe mailing list