From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 72E3BBBC1 for ; Fri, 14 Mar 2008 12:33:48 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArYAAIz/2UfPn3g8n2dsb2JhbACBWo8mAQEBAQEGBAYJCBiYJw X-IronPort-AV: E=Sophos;i="4.25,501,1199660400"; d="scan'208";a="10266585" Received: from nn6.excitenetwork.com (HELO excite.com) ([207.159.120.60]) by mail3-smtp-sop.national.inria.fr with ESMTP; 14 Mar 2008 12:33:47 +0100 Received: by xprdmxin.myway.com (Postfix, from userid 110) id 42D4E8B313; Fri, 14 Mar 2008 07:33:46 -0400 (EDT) To: alain@frisch.fr Subject: Re: [Caml-list] BDDs in ocaml Received: from [132.230.166.192] by xprdmailfe17.nwk.excite.com via HTTP; Fri, 14 Mar 2008 07:33:46 EST X-AntiAbuse: This header was added to track abuse, please include it with any abuse report X-AntiAbuse: ID = 8a8a82c06e1c8d4366ddc3f449c5aa61 Reply-To: sasha.mal@excite.com From: "sasha mal" MIME-Version: 1.0 X-Sender: sasha.mal@excite.com X-Mailer: PHP Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Cc: caml-list@yquem.inria.fr Message-Id: <20080314113346.42D4E8B313@xprdmxin.myway.com> Date: Fri, 14 Mar 2008 07:33:46 -0400 (EDT) X-Spam: no; 0.00; bdds:01 ocaml:01 abstraction:01 subset:01 bdds:01 frisch:01 frisch:01 ocaml:01 implements:01 excite:98 excite:98 wrote:01 wrote:01 caml-list:01 caml-list:01 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!