BDD package in Ada.

BDD package in Ada.

[Vincent DIEMUNSCH]

Hello everybody,

Binary Decisions Diagram [1] is a key technology in computer science, for the verification of software and hardware designs.  Donald Knuth calls BDDs "one of the only really fundamental data structures that came out in the last twenty-five years" and mentions that Bryant's 1986 paper was for some time one of the most-cited papers in computer science.

There are many BDD libraries in C/C++, there are libraries in Lisp, Python, Java, Lua, OCaml, Prolog... all available on the Internet [2], but I couldn't find one in Ada. I am pretty sure that there must be excellent BDD libraries in Ada used in the Defense Industry, but it seems that no one is public.

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 ? 

Regards,

Vincent Diemunsch


[1] - http://en.wikipedia.org/wiki/Binary_decision_diagram
[2] - https://github.com/johnyf/tool_lists/blob/master/bdd.md

Re: BDD package in Ada.

[Dmitry A. Kazakov]

On Tue, 7 Apr 2015 13:35:53 -0700 (PDT), Vincent DIEMUNSCH wrote:

> Binary Decisions Diagram [1] is a key technology in computer science, for
> the verification of software and hardware designs.  Donald Knuth calls
> BDDs "one of the only really fundamental data structures that came out in
> the last twenty-five years" and mentions that Bryant's 1986 paper was for
> some time one of the most-cited papers in computer science.

I would not call it "fundamental". It is simply a tree with factored out
subtrees. Need not to be binary, BTW.

IMO, factoring out similar subtrees is merely a technique to save memory
and reduce overheard of some computations over the graph nodes. Sometimes
it pays off, sometimes it does not.

As for decision trees, they were known and used in AI for I don't know how
long, ever.

> There are many BDD libraries in C/C++, there are libraries in Lisp,
> Python, Java, Lua, OCaml, Prolog... all available on the Internet [2], but
> I couldn't find one in Ada. I am pretty sure that there must be excellent
> BDD libraries in Ada used in the Defense Industry, but it seems that no
> one is public.

Of course there exist Ada implementations. I have one in Ada

http://www.dmitry-kazakov.de/ada/fuzzy_ml_api.htm#Fuzzy.Graph

with binary and general case nodes.

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

I don't think structures like trees and directed graphs could be packed in
a library. Each application of graphs is very specific. The abstraction
level is too low to make it a decent container. Memory management is always
different. Operations are always different. The impact of the
representation is so huge that different application almost always require
a different implementation.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: BDD package in Ada.

[Vincent DIEMUNSCH]

Le mercredi 8 avril 2015 08:38:19 UTC+2, Dmitry A. Kazakov a écrit :
 
> I would not call it "fundamental". It is simply a tree with factored out
> subtrees. Need not to be binary, BTW.
A BINARY decision diagram needs to be binary, by definition. It is not "simply" a tree, but a highly optimised data structure, not only by factoring the tree, but through variable ordering, which is the key idea. (Briant's paper is about ORDERED BDD). It is usefull for the implementation of Sets and operations on sets. 

 
> Of course there exist Ada implementations. I have one in Ada
> http://www.dmitry-kazakov.de/ada/fuzzy_ml_api.htm#Fuzzy.Graph
> with binary and general case nodes.
I see a general object oriented frame for creating graphs... Very different from a Reduced Ordered Binary Decision Diagram Library.

> I don't think structures like trees and directed graphs could be packed in
> a library. Each application of graphs is very specific. The abstraction
> level is too low to make it a decent container. Memory management is always
> different. Operations are always different. The impact of the
> representation is so huge that different application almost always require
> a different implementation.

I agree. And this is why I need a Library carefully optimised for the special case of ROBDD.

Regards,

Vincent

Re: BDD package in Ada.

[jan.de.kruyf]

Hallo,
Here is a link to Knuth's musings on the subject:

http://www.cs.utsa.edu/~wagner/knuth/fasc1b.pdf

There is some youtube thing around as well.

Cheers,
j.

Re: BDD package in Ada.

[vincent.diemunsch]

Le mercredi 8 avril 2015 14:25:37 UTC+2, jan.de...@gmail.com a écrit :
> Hallo,
> Here is a link to Knuth's musings on the subject:
> 
> http://www.cs.utsa.edu/~wagner/knuth/fasc1b.pdf
> 
> There is some youtube thing around as well.
> 
> Cheers,
> j.

Thank you for the link. It sounds very interesting. Is it free to read it ?
Kind regards,

Vincent

Re: BDD package in Ada.

[jan.de.kruyf]

On Wednesday, April 8, 2015 at 8:39:21 PM UTC+2, vincent....@gmail.com wrote:

> 
> Thank you for the link. It sounds very interesting. Is it free to read it ?
> Kind regards,
> 
> Vincent

It is the pre-publication version, with warts and all.
It is a service of Knuth to himself and to us.
If you take the filename off the link you will find the other pre-publication parts of volume 4 .

cheers,

j.

Re: BDD package in Ada.

[jan.de.kruyf]

On Wednesday, April 8, 2015 at 8:39:21 PM UTC+2, vincent....@gmail.com wrote:

> 
> Thank you for the link. It sounds very interesting. Is it free to read it ?
> Kind regards,
> 
> Vincent


Vincent,
I managed to make a pdf / dvi out of one of Knuths Literate Programming files.

http://www-cs-faculty.stanford.edu/~uno/programs.html#bdd12

if you want I can send it to you.

cheers,

j.

Re: BDD package in Ada.

[vincent.diemunsch]

Le jeudi 9 avril 2015 18:51:23 UTC+2, jan.de...@gmail.com a écrit :
> On Wednesday, April 8, 2015 at 8:39:21 PM UTC+2, vincent....@gmail.com wrote:
> 
> > 
> > Thank you for the link. It sounds very interesting. Is it free to read it ?
> > Kind regards,
> > 
> > Vincent
> 
> 
> Vincent,
> I managed to make a pdf / dvi out of one of Knuths Literate Programming files.
> 
> http://www-cs-faculty.stanford.edu/~uno/programs.html#bdd12
> 
> if you want I can send it to you.
> 
> cheers,
> 
> j.

Is it about BDDs ? Yes I would be pleased to read it.

Vincent

Re: BDD package in Ada.

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1923 bytes --]

"Vincent DIEMUNSCH" <vincent.diemunsch@gmail.com> wrote in message 
news:c7db12c1-10fa-40ee-a2df-ff8a8b2177bc@googlegroups.com...
>Le mercredi 8 avril 2015 08:38:19 UTC+2, Dmitry A. Kazakov a écrit :

>> I would not call it "fundamental". It is simply a tree with factored out
>> subtrees. Need not to be binary, BTW.
>A BINARY decision diagram needs to be binary, by definition. It is not 
>"simply" a tree,
> but a highly optimised data structure, not only by factoring the tree, but 
> through variable
> ordering, which is the key idea. (Briant's paper is about ORDERED BDD). It 
> is usefull
> for the implementation of Sets and operations on sets.

Sounds like premature optimization to me. If you want sets, use 
Ada.Containers.Ordered_Sets and see if it is fast enough. In the unlikely 
case that it is not, implement your own body to a similar specification 
using a different technology to handle the ordering.

The vast majority of uses of anything do not need "highly optimized" data 
structures. On top of which, it's likely that your implementer has spent 
plenty of time optimizing the standard containers, so it's quite likely that 
they will be faster than you might expect.

That's a lesson we all need to learn, and re-learn, and re-learn again, 
because "highly optimized data structures" are a lot more fun and satisfying 
to a programmer. But they're rarely actually needed. (I've made that mistake 
plenty of times.)

[Side note to another thread. That of course goes for GC as well. There is 
lots of junkware that doesn't need to be engineered well; that's why dynamic 
languages have such a following. But that's not Ada's target market.]

Whatever BDD is, it can't be very important since I've never heard of it 
until today. :-) I'm pretty sure I would have run across something that's 
actually fundamental in 30 years. YMMV.

                                                           Randy.

Re: BDD package in Ada.

[Paul Rubin]

"Randy Brukardt" <randy@rrsoftware.com> writes:
> [Side note to another thread. That of course goes for GC as
> well. There is lots of junkware that doesn't need to be engineered
> well; that's why dynamic languages have such a following. But that's
> not Ada's target market.]

I'd say Ada's target market has shrunk in the last few decades, to the
realtime systems and embedded control sectors.  The remaining sector of
big server-side non-realtime systems (a buddy of mine used to work on
those) has been mostly ceded to Java, which is garbage collected.  GC's
main benefits are when the program is complicated enough that manual
memory management increases development effort significantly and makes
bugs more likely.  It's less of an issue in simpler programs, especially
those that don't need dynamic memory.

> Whatever BDD is, it can't be very important since I've never heard of
> it until today. :-) I'm pretty sure I would have run across something
> that's actually fundamental in 30 years. YMMV.

Knuth's remark was there are few fundamental data structures that
haven't been around for longer than 30 years, and BDD's are among the
exceptions.

Re: BDD package in Ada.

[gautier_niouzes]

Le jeudi 9 avril 2015 01:40:08 UTC+2, Paul Rubin a écrit :

> I'd say Ada's target market has shrunk in the last few decades, to the
> realtime systems and embedded control sectors.  The remaining sector of
> big server-side non-realtime systems (a buddy of mine used to work on
> those) has been mostly ceded to Java, which is garbage collected.  GC's
> main benefits are when the program is complicated enough that manual
> memory management increases development effort significantly and makes
> bugs more likely.  It's less of an issue in simpler programs, especially
> those that don't need dynamic memory.

This seems to suggest there are only GC and manual memory management as alternatives. Ada provides a third way in this respect with controlled types.
Just my two centimes ;-)
G.

Re: BDD package in Ada.

[Randy Brukardt]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1662 bytes --]

<gautier_niouzes@hotmail.com> wrote in message 
news:7136971a-4bc8-4f42-a605-5a37127ca4a9@googlegroups.com...
Le jeudi 9 avril 2015 01:40:08 UTC+2, Paul Rubin a écrit :

>> I'd say Ada's target market has shrunk in the last few decades, to the
>> realtime systems and embedded control sectors.  The remaining sector of
>> big server-side non-realtime systems (a buddy of mine used to work on
>> those) has been mostly ceded to Java, which is garbage collected.  GC's
>> main benefits are when the program is complicated enough that manual
>> memory management increases development effort significantly and makes
>> bugs more likely.  It's less of an issue in simpler programs, especially
>> those that don't need dynamic memory.

>This seems to suggest there are only GC and manual memory management as
>alternatives. Ada provides a third way in this respect with controlled 
>types.
>Just my two centimes ;-)

As I noted before, Ada provides at least 5 ways to manage dynamic memory:
(1) Stack
(2) Container
(3) Controlled types (as in Smart Pointers)
(4) Subpools (perhaps "semi-manual")
(5) Traditional allocate/deallocate

There's nothing "manual" about the first three from the perspective of a 
client (programmer). GC proponents complain about the work to create things 
like (1), (2), and (3) -- but there is no work for Ada programmers when you 
are using language capabilities or widely available libraries. Most people 
shouldn't be creating containers -- there's no point, you'll have a hard 
time doing better than the language-defined ones, and your time could be 
better used doing something else.

                                     Randy.

Re: BDD package in Ada.

[Georg Bauhaus]

On 08.04.15 23:30, Randy Brukardt wrote:
> "Vincent DIEMUNSCH" <vincent.diemunsch@gmail.com> wrote in message
> news:c7db12c1-10fa-40ee-a2df-ff8a8b2177bc@googlegroups.com...
>> Le mercredi 8 avril 2015 08:38:19 UTC+2, Dmitry A. Kazakov a �crit :
>
>>> I would not call it "fundamental". It is simply a tree with factored out
>>> subtrees. Need not to be binary, BTW.
>> A BINARY decision diagram needs to be binary, by definition. It is not
>> "simply" a tree,
>> but a highly optimised data structure, not only by factoring the tree, but
>> through variable
>> ordering, which is the key idea. (Briant's paper is about ORDERED BDD). It
>> is usefull
>> for the implementation of Sets and operations on sets.
>
> Sounds like premature optimization to me.

The presentations say that in the worst case, some fundamental operations
are O(linear) if the graph is ordered, but are O(exponential) if not.
I am not sure, then, if that makes "premature optimization" an adequate
characterization.

If a compiler needs to sort out whether or not something-and-then-this-and-...
-then-if-that...-and-finally-this, then wouldn't the above ordering of Boolean
trees have a major impact on feasibility?

Re: BDD package in Ada.

[Dmitry A. Kazakov]

On Thu, 09 Apr 2015 11:06:18 +0200, Georg Bauhaus wrote:

> On 08.04.15 23:30, Randy Brukardt wrote:
>> "Vincent DIEMUNSCH" <vincent.diemunsch@gmail.com> wrote in message
>> news:c7db12c1-10fa-40ee-a2df-ff8a8b2177bc@googlegroups.com...
>>> Le mercredi 8 avril 2015 08:38:19 UTC+2, Dmitry A. Kazakov a �crit :
>>
>>>> I would not call it "fundamental". It is simply a tree with factored out
>>>> subtrees. Need not to be binary, BTW.
>>> A BINARY decision diagram needs to be binary, by definition. It is not
>>> "simply" a tree,
>>> but a highly optimised data structure, not only by factoring the tree, but
>>> through variable
>>> ordering, which is the key idea. (Briant's paper is about ORDERED BDD). It
>>> is usefull for the implementation of Sets and operations on sets.
>>
>> Sounds like premature optimization to me.
> 
> The presentations say that in the worst case, some fundamental operations
> are O(linear) if the graph is ordered, but are O(exponential) if not.
> I am not sure, then, if that makes "premature optimization" an adequate
> characterization.
>
> If a compiler needs to sort out whether or not something-and-then-this-and-...
> -then-if-that...-and-finally-this, then wouldn't the above ordering of Boolean
> trees have a major impact on feasibility?

For decision threes even more important is the order in which features
(questions at the nodes) get tested, both in terms of complexity and the
results obtained when some choices are implied (missing nodes). Therefore
trees are frequently rotated to change the order. Everybody knows this
problem from programming when writes nested if's and/or cases. Which
variable to test first? The code greatly depends on the order, as well as
ability to factor out common paths.

With low-level structures, you never can tell what is optimization and what
is a property. That is why there are many graph implementation but when you
need one, you have to design it new.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: BDD package in Ada.

[Randy Brukardt]

"Georg Bauhaus" <bauhaus@futureapps.invalid> wrote in message 
news:mg5fcg$maf$1@dont-email.me...
> On 08.04.15 23:30, Randy Brukardt wrote:
>> "Vincent DIEMUNSCH" <vincent.diemunsch@gmail.com> wrote in message
>> news:c7db12c1-10fa-40ee-a2df-ff8a8b2177bc@googlegroups.com...
>>> Le mercredi 8 avril 2015 08:38:19 UTC+2, Dmitry A. Kazakov a ?crit :
>>
>>>> I would not call it "fundamental". It is simply a tree with factored 
>>>> out
>>>> subtrees. Need not to be binary, BTW.
>>> A BINARY decision diagram needs to be binary, by definition. It is not
>>> "simply" a tree,
>>> but a highly optimised data structure, not only by factoring the tree, 
>>> but
>>> through variable
>>> ordering, which is the key idea. (Briant's paper is about ORDERED BDD). 
>>> It
>>> is usefull
>>> for the implementation of Sets and operations on sets.
>>
>> Sounds like premature optimization to me.
>
> The presentations say that in the worst case, some fundamental operations
> are O(linear) if the graph is ordered, but are O(exponential) if not.
> I am not sure, then, if that makes "premature optimization" an adequate
> characterization.

That's pretty much the definition of premature optimization. Everything 
interesting is O(exponential) when you start out.

> If a compiler needs to sort out whether or not 
> something-and-then-this-and-...
> -then-if-that...-and-finally-this, then wouldn't the above ordering of 
> Boolean
> trees have a major impact on feasibility?

It depends on N. Most N's are small. The Janus/Ada optimizer is (worst-case) 
O(N**4). It proved to be easier to manage N than to try to redo it to reduce 
that to a smaller O. Part of the problem of course is that the constant 
factor matters in practice. If the runtime of the original version is 
10*(N**4), but the new version is 1000*(N**2), you will need pretty large Ns 
before you'll gain anything. In the Janus/Ada case, N (size of a code tree) 
has to be over 2000 before the runtime becomes noticable to a human. The 
average N is around 200, only large aggregates or giant case statements give 
those massive Ns that cause trouble.

That's why almost all optimization is premature. I would never have guessed 
right on the distribution of Ns or what is important in our compiler. I 
would have wasted time on resolution and other areas whose time was 
essentially irrelevant. (And I probably did at some point. ;-) The biggest 
performance problem in our early Ada 95 compilers turned out to be a 
premature optimization that didn't work (but had a lot of overhead). I only 
figured that out when I got tired of waiting for a long compilation and 
stuck a profiler on the appropriate part of the compiler. (I had thought it 
was doing something useful.)

                                         Randy.


                                               Randy.

Re: BDD package in Ada.

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1miph3v72f4y2$.1u76w2ujg74zf$.dlg@40tude.net...
...
> I don't think structures like trees and directed graphs could be packed in
> a library.

Of course, Ada has Ada.Containers.Multiway_Trees, so it's pretty clear that 
trees *can* be in a library. It wouldn't be hard to do something similar for 
more general directed graphs. Whether that's useful or not I'll leave others 
to judge. (It does match many things in my work, but nothing since it was 
added to Ada, so I've never had an opportunity to use it.)

                                         Randy.

Re: BDD package in Ada.

[Per Sandberg]

[-- Attachment #1: Type: text/plain, Size: 1382 bytes --]


Played a bit with a binding and ended up with the following.
GCC 4.9 should work.
/Per



Den 2015-04-07 22:35, Vincent DIEMUNSCH skrev:
> Hello everybody,
>
> Binary Decisions Diagram [1] is a key technology in computer science, for the verification of software and hardware designs.  Donald Knuth calls BDDs "one of the only really fundamental data structures that came out in the last twenty-five years" and mentions that Bryant's 1986 paper was for some time one of the most-cited papers in computer science.
>
> There are many BDD libraries in C/C++, there are libraries in Lisp, Python, Java, Lua, OCaml, Prolog... all available on the Internet [2], but I couldn't find one in Ada. I am pretty sure that there must be excellent BDD libraries in Ada used in the Defense Industry, but it seems that no one is public.
>
> 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 ?
>
> Regards,
>
> Vincent Diemunsch
>
>
> [1] - http://en.wikipedia.org/wiki/Binary_decision_diagram
> [2] - https://github.com/johnyf/tool_lists/blob/master/bdd.md
>

[-- Attachment #2: cudd.tgz --]
[-- Type: application/x-compressed-tar, Size: 1129 bytes --]

Re: BDD package in Ada.

[Paul Rubin]

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.

Re: BDD package in Ada.

[vincent.diemunsch]

Le jeudi 9 avril 2015 17:24:14 UTC+2, Paul Rubin a écrit :
> 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 ?

I thought of using BDD for : 
- solving typical SAT problems, without the need to use an external SAT,
solver (in fact I thought it could be much simpler to use BDD than 
developing a SAT solver !).
- Sets and relations problems. 

> Is the BDD library itself likely to be used inside a critical system?
No, not inside. But since BDD is a key technology for Model Checking
it is still related to critical systems, as a tool for checking them precisely.

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

It is true that finding the best variable ordering is NP-hard, so a SAT
solver is required, but I think that most implementations use heuristics
to find a «good» ordering. 

Re-implementing MiniSAT in Ada, that's a lot more challenging than
developing a BDD library ! :-).

Vincent