Re: BDD package in Ada.

[vincent.diemunsch@gmail.com]

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