[Caml-list] BDDs in ocaml

[sasha mal]

Dear all,

I wonder whether anyone has a BDD (binary decision diagram) implementation in ocaml. Ocaml interfaces to external BDD implementations in other languages (like Cudd) are of no use to me.

Thanks a lot and best regards

Sasha.

_______________________________________________
Join Excite! - http://www.excite.com
The most personalized portal on the Web!

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Pietro Abate]

On Thu, Mar 13, 2008 at 08:34:46AM -0400, sasha mal wrote:
> I wonder whether anyone has a BDD (binary decision diagram)
> implementation in ocaml. Ocaml interfaces to external BDD
> implementations in other languages (like Cudd) are of no use to me.

have a look at this paper for a non-optimized bdd implementation from
Jean-Christophe Filliatre.
http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz

I don't know if the full source code is avalaible. I wasn't able to
find it. It would be interesting to repeat their experiments and play
with it.

:)
p

[Berke Durak]

sasha mal a écrit :

> Dear all,
>
>
>
> I wonder whether anyone has a BDD (binary decision diagram) implementation in ocaml. Ocaml interfaces to external BDD implementations in other languages (like Cudd) are of no use to me.
>
>

Hello,

There is one small BDD module written by Xavier Leroy for an experimental SAT-solver
during the EDOS project:

https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/xlsat/?root=sodiac

--
Berke DURAK

[Jean-Christophe Filliâtre]

Pietro Abate a écrit :

> On Thu, Mar 13, 2008 at 08:34:46AM -0400, sasha mal wrote:
>> I wonder whether anyone has a BDD (binary decision diagram)
>> implementation in ocaml.
>

> have a look at this paper for a non-optimized bdd implementation from
> Jean-Christophe Filliatre.
> http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz
>
> I don't know if the full source code is avalaible.

I wrote the code by that time, but I was too lazy to package it.
Here it is:

http://www.lri.fr/~filliatr/ftp/ocaml/bdd/

Hope this helps,
--
Jean-Christophe

[Olivier Michel]

On Thu, Mar 13, 2008 at 02:14:43PM +0100, Berke Durak wrote:
> sasha mal a écrit :
> >Dear all,
> >
> >
> >
> >I wonder whether anyone has a BDD (binary decision diagram) implementation
> >in ocaml. Ocaml interfaces to external BDD implementations in other
> >languages (like Cudd) are of no use to me.
> >
> >
>
> Hello,
>
> There is one small BDD module written by Xavier Leroy for an experimental
> SAT-solver
> during the EDOS project:
>
> https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/xlsat/?root=sodiac
>
>

Hello,

I once wrote in the 90s a (RO)BDD implementation in caml-light (the
translation to Ocaml should not be a big deal though) for the
development of the declarative data-parallel language 8,5. The sources
(unfortunately with comments in French, but they are pretty much
straightforward!) are available here:

http://www.ibisc.univ-evry.fr/~michel/BDD/

Regards,
Olivier MICHEL.

--
Olivier MICHEL Email : mic...@ibisc.univ-evry.fr
Universite d'Evry Val d'Essonne http : www.ibisc.univ-evry.fr/~michel
Lab. IBISC - LIS project http : mgs.ibisc.univ-evry.fr
FRE 3190 of CNRS and Genopole Phone : +33 (0)1.60.87.39.10
523, place des terrasses de l'agora Fax : +33 (0)1.60.87.37.89
91000 Evry - FRANCE

[Alain Frisch]

sasha mal wrote:
> I wonder whether anyone has a BDD (binary decision diagram)
> implementation in ocaml. Ocaml interfaces to external BDD
> implementations in other languages (like Cudd) are of no use to me.

I've seen many implementation of BDDs in OCaml, but none of them
implements automatic reordering of variables (which is by far the most
complex part of serious BDD packages). For some applications, this is
really a must. Why is it impossible for you to use to an external BDD
implementation?

-- Alain

[sasha mal]

Hi Alain!

Essentially, an intermediate goal is to enhance an existing BDD implementation with several methods (they are needed inside a model-checker). One method should count the exact size of the support of a boolean function. Cudd, for instance, doesn't to this exactly (returns a double). Second, I'd like to implement Cartesian abstraction with respect to blocks of variables. I.e. given a boolean function on variables

x11,...,x1m,x21,...,x2m, ... ,xn1,...,xnm

that represents a subset Y of (2^m)^n

we have to compute the boolean function that represents

projection_{x11,...,x1m}(Y) x projection_{x21,...,x2m}(Y) x ... x projection_{xn1,...,xnm}(Y).

A most simple BDD representation with best asymptotic times would be good to start with. Variable reordering, for instance, is of no use; ever sharing among different BDDs on the same computer is an obstacle.

Best regards

Sasha.

--- On Fri 03/14, Alain Frisch < al...@frisch.fr > wrote:

From: Alain Frisch [mailto: al...@frisch.fr]

To: sash...@excite.com

Cc: caml...@yquem.inria.fr

Date: Fri, 14 Mar 2008 08:38:41 +0100

Subject: Re: [Caml-list] BDDs in ocaml

sasha mal wrote:> I wonder whether anyone has a BDD (binary decision diagram)> implementation in ocaml. Ocaml interfaces to external BDD> implementations in other languages (like Cudd) are of no use to me.I've seen many implementation of BDDs in OCaml, but none of them implements automatic reordering of variables (which is by far the most complex part of serious BDD packages). For some applications, this is really a must. Why is it impossible for you to use to an external BDD implementation?-- Alain

_______________________________________________
Join Excite! - http://www.excite.com
The most personalized portal on the Web!