English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Re: [Caml-list] BDDs in ocaml
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2008-03-14 (11:33)
From: sasha mal <sasha.mal@e...>
Subject: Re: [Caml-list] BDDs in ocaml

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


 --- 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!