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

[Denis Bueno]

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.

-- 
 Denis
-------------- next part --------------
A non-text attachment was scrubbed...
Name: ParseCnf.hs
Type: application/octet-stream
Size: 2268 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20080211/6a18ee3c/ParseCnf.obj
-------------- next part --------------
A non-text attachment was scrubbed...
Name: MicroSat.hs
Type: application/octet-stream
Size: 6674 bytes
Desc: not available
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20080211/6a18ee3c/MicroSat.obj