BDDs in ocaml

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!

Re: [Caml-list] BDDs in ocaml

[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

Re: [Caml-list] BDDs in ocaml

[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

Re: [Caml-list] BDDs in ocaml

[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

Re: [Caml-list] BDDs in ocaml

[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 : michel@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

Re: [Caml-list] BDDs in ocaml

[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

Re: [Caml-list] BDDs in ocaml

[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 < alain@frisch.fr > wrote:

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

To: sasha.mal@excite.com

     Cc: caml-list@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!

Re: [Caml-list] BDDs in ocaml

[sasha mal]

Thanks a lot!

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