From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: BDD package in Ada.
Date: Thu, 09 Apr 2015 08:24:12 -0700
Organization: A noiseless patient Spider
Message-ID: <87k2xle34z.fsf@jester.gateway.sonic.net>
References: <44b2e375-8993-4a7e-b81a-6a7b512d2e3e@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: mx02.eternal-september.org;
 posting-host="bda44be170c76b3ef6d23fecd204a8fa";
	logging-data="7207"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+0tPMVsmZbg7IlksXRlz8G"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux)
Cancel-Lock: sha1:TesHl8nwKZdWRvek2MAqjLL0c14=
	sha1:6XvRmR+GOrGqlIvqdmgzCV7e/Ts=
Xref: news.eternal-september.org comp.lang.ada:25491
Date: 2015-04-09T08:24:12-07:00
List-Id: <comp.lang.ada>

Vincent DIEMUNSCH <vincent.diemunsch@gmail.com> writes:
> Binary Decisions Diagram [1] is a key technology in computer science,...
> So I hesitate between developping a binding to an existing C library,
> and thus having access to the best and fastest implementations, or
> developping one myself, but the result might be less efficient,
> although easier to use from Ada and more portable.
> Any piece of advice to give me ? Would some of you be interested in
> using it ? In contributing to the development as an Open Source ?

This sounds interesting.  I had heard of BDD before but didn't know what
they were.  One thing I'd ask is what your goals are: do you want to use
BDD's for something?  To write an interesting Ada library?  To get other
people interested in BDD's?

Is the BDD library itself likely to be used inside a critical system?
If yes, that speaks in favor of writing it in Ada.  Or is most of the
library about taking some decision structure and converting it to a BDD
for use someplace else?  In that case, maybe it's simplest to bind an
existing library, especially if writing a new one duplicates a lot of
effort.

I get the impression from the Wikipedia article that a lot of the work
in the library is heuristically finding a good ordering of the
variables.  I wonder if you can use an existing SAT or SMT solver for
that, and in fact whether the existing BDD libraries work that way.
CVC3 and Z3 are the SMT solvers I hear the most about right now (haven't
heard any mentions of Yices for a while).  Both of them are written in
C++.  I'm not really conversant with this technology though I think it
is very important and I want to try it out.  I don't know whether pure
SAT solvers are actively developed these days, though MiniSAT has been
around forever and has been used in some interesting things.  IIRC, it
is written in C and it is very simple (but still effective).
Re-implementing it in Ada as part of a BDD library might be interesting.