[Haskell-cafe] RFC: SAT solver using Cont/callCC for backtracking
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!
More information about the Haskell-Cafe