[Haskell-cafe] RFC: SAT solver using Cont/callCC for backtracking
search
Denis Bueno
dbueno at gmail.com
Mon Feb 11 17:03:55 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.
--
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
More information about the Haskell-Cafe
mailing list