tulip-control / dd

Binary Decision Diagrams (BDDs) in pure Python and Cython wrappers of CUDD, Sylvan, and BuDDy
https://pypi.org/project/dd
Other
178 stars 39 forks source link

Method for obtaining the paths from leaves to root #51

Closed glarange closed 4 years ago

glarange commented 4 years ago

Hi @slivingston @johnyf , great lib, especially interested in dd.

I was trying to find or add a method for discovering all paths from "true" leaves all way up to root (sometimes called cutsets). For example, attached .

https://github.com/glarange/BDD/blob/master/fig_5_.paths.pdf https://github.com/glarange/BDD/blob/master/fig_4_Paths.pdf

Most BDD applications I've seen are related to circuit design or mapping. Cutsets have applications in reliability theory, probabilistic contingency analysis (for nuclear reactors or electric grid, etc.) Once you find all paths, you can assign probabilities to nodes and finding the exact probability of the top event (root), or failure, becomes trivial.

First step would be to find parent nodes ending in "true" leaves. I've indicated such nodes in fig 4 and 5 above.

Is there a method in dd that does something similar? Or if not, could you point me in the right direction to add such a method?

Thanks, Gui

glarange commented 4 years ago

Might be easier if I attach the examples. Gui

fig5.paths.pdf fig_4_Paths.pdf

johnyf commented 4 years ago

The method dd.bdd.BDD.pick_iter computes all satisfying assignments, which are paths from the root to the constant node TRUE. It may be used as an example for a computation that involves a set of paths.

https://github.com/tulip-control/dd/blob/f9aa4d1a09c286de769bde17dd92ece63cf4c3d9/dd/bdd.py#L1102-L1144

https://github.com/tulip-control/dd/blob/f9aa4d1a09c286de769bde17dd92ece63cf4c3d9/dd/bdd.py#L1415-L1435

The computation in dd.bdd is the Python implementation. If an implementation for dd.cudd would be of interest, then an implementation at the level of the dd.cudd and dd.autoref API would work for both dd.cudd and dd.autoref. The module dd._copy has functions that use this API, for example:

https://github.com/tulip-control/dd/blob/f9aa4d1a09c286de769bde17dd92ece63cf4c3d9/dd/_copy.py#L45-L76

glarange commented 4 years ago

Yes, actually, _pickiter seems to be what I'm looking for. But what's u in the syntax? I was trying to use it as below:

` from dd import autoref as _bdd bdd = _bdd.BDD() bits = ('x', 'y', 'z') for var in bits: bdd.add_var(var) u = bdd.add_expr('(x /\ y) \/ (x /\ z) \/ (y /\ z) ') bdd.collect_garbage() bdd.dump('fig5.paths.pdf')

v = bdd._bdd.pick_iter('x') print(v) `

The method dd.bdd.BDD.pick_iter computes all satisfying assignments, which are paths from the root to the constant node TRUE. It may be used as an example for a computation that involves a set of paths.

glarange commented 4 years ago

Hi Ioannis,

The pick.iter worked nicely with cudd. But not so with sylvan. Any suggestions would be highly appreciated. Thanks once more! G Capture_sylvan_not_implemented

johnyf commented 4 years ago

The u in the syntax is an instance dd.autoref.Function when calling dd.autoref.BDD.pick_iter and a dd.cudd.Function when calling dd.cudd.BDD.pick_iter. For example, the method BDD.add_expr returns a Function instance.

johnyf commented 4 years ago

Please see https://github.com/tulip-control/dd/issues/55#issuecomment-646575348.