RFC: SAT solver using Cont/callCC for backtracking search
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
dbueno:
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, http://hackage.haskell.org/cgi-bin/hackage-scripts/package/sat-1.1.1 so feel free to upload this code! -- Don
On Mon, Feb 11, 2008 at 5:05 PM, Don Stewart
Have you thought about uploading it to hackage.haskell.org? We've got some similar stuff up there already,
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/sat-1.1.1
so feel free to upload this code!
Thanks. There's one more optimisation (clause learning) described in the paper that I intend to implement first. Then I'd like to upload it to hackage. If, after all that, I still feel adventurous, I may implement 2-watched literals. At that point it might actually be a competitive solver. But we'll see. -- Denis
On Mon, Feb 11, 2008 at 5:05 PM, Don Stewart
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: http://hackage.haskell.org/cgi-bin/hackage-scripts/package/sat-micro-hs-0.1 -- Denis
participants (2)
-
Denis Bueno -
Don Stewart