Converting BDD to ROBDD

Question

When converting BDD to ROBDD in my solution can I apply elimination rule for States whose high(v)=0 eliminate them? Or should it compulsory in ROBDD on every level there must be exactly to nodes.

Answer 1

To avoid confusion: BDDs have nodes, not states (otherwise, you may get confused when BDDs are used to store transition systems that have states). 

The elimination rule used for BDD says that (x?φ:φ) is replaced with φ to avoid this unnecessary case distinction.  In contrast, the elimination rule of ZDDs use another elimination rule which replaces (x?false:φ) with φ. As (x?false:φ) is equivalent to ¬x⋀φ and x is not shown, ZDDs are called zero-suppressed DDs. FDDs have accidentally the same elimination rule as ZDDs, but FDDs have another decomposition rule.

The elimination should be done recursively bottom up, i.e., as follows (written in F#):

let rec ReduceBDD b =
    if b=0 then 0
    elif b=1 then 1
    else
        let b0 = ReduceBDD b.lowChild    
        let b1 = ReduceBDD b.hghChild
        if b0=b1 then b0 else MkNode(b.var,b1,b0)

MkNode must thereby also check whether the node that shall be created here already exists, and if so, it should return the existing node. 

Does this help?

Comments

yes it does. thank you :)