[Haskell-cafe] RFC: SAT solver using Cont/callCC for backtracking
dbueno at gmail.com
Tue Feb 26 23:55:38 EST 2008
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:
More information about the Haskell-Cafe