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

[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

[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

[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