avalaible bdd libraries

UPDATE

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 .

Ocaml libraries (bindings and native) :

  • Jean-Christophe Filliâtre (ocaml implementation) Paper Code

  • 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

C/C++ Libraries

Other Languages

Relevant Mailing list Messages

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.