I’ve just released the new version of ocaml-buddy, my ocaml bindings to the buddy BDD c library. Thanks to a fruitful interaction with Jimmy Thomson, I’ve fixed a couple of memory leaks and cleaned up the code a bit.
grab it when is still hot : https://github.com/abate/ocaml-buddy/tree/0.5
comments a testers are welcome. A debian package is on the way
I’ve taken some time off to finish the ocaml bindings to Buddy BDD.
This code is a fork of the bindings downloaded from http://nicosia.is.s.u-tokyo.ac.jp/members/hagiya/xml/readme.htm#buddy .The original authors are Akihiko Tozawa and Masami Hagiya and they granted me - via personal communication - the right to release the software as open source.
I’ve added documentation to the .mli (mostly from the buddy website), few functions that were missed in the original work, the build system and an example.
I’ve released the code under GPLv3 . The code is available on github. This snapshot compiles cleanly on debian unstable with the package libbdd-dev installed. There is a micro example in the source. I plan to use the bindings with some real world data in the next few weeks. Debian package is work in progress.
Enjoy. As always feedback is welcome.
In the end I found ocaml bindings for the Buddy BDD library. yuppi \o/
BDDs or Binary Decision Diagrams are a method of representing boolean expressions. I searched the net for available BDD libraries (I’ve considered different BDD variants in my research). In particular I focused on OCaml implementations. My conclusion is that as today there is no viable native implementation of an efficient bdd library. It seems common knowledge (take this cum granis salis , I haven’t done any work in this direction) that the fastest bdd library is buddy, but there are not OCaml bindings to it.
Next step would be to run few tests and to evaluate the available OCaml implementations.
These are my findings. I’m sure the list is not exhaustive, also because many bdd implementations are usually anonymously embedded as part of larger projects. In particular the model checking community and the planning community do extensive use of BDDs :
First of all what is a bdd : Wikipedia .
bindings to the CUDD BDD library Code
Olivier Michel (ocaml implementation) Code
Xavier Leroy (part of an experimental sat solver) Code
John Harrison Code
Ocaml implementation (who is the author ?) Wiki
many others in the wikipedia reference section of the bdd article…
The ocaml ml has several references to BDDs. These are 3 interesting threads that I’ve used as a starting point for my research.
In this Thread there is mention of a possible binding for Jørn Lind-Nielsen’s BDD library BuDDy. I’m wondering if this binding was ever released.
In this Thread Alain Frish points out that none of existing ocaml libraries implements automatic reordering of variables… And I don’t know if the state of affairs is changed at this regard.
In this Thread David Mentre announces a preliminary work on binding for the cudd library, but the link is broken… and there is a mention to a caml-light implementation of a robdd library that I was also not able to retrieve.