Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.3k answers

1.7k comments

556 users

+1 vote
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.
in # Study-Organisation (Master) by (190 points)

1 Answer

+2 votes

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?

by (170k points)
yes it does. thank you :)

Related questions

0 votes
1 answer
0 votes
1 answer
asked Aug 13, 2022 in # Study-Organisation (Master) by yk (2.7k points)
0 votes
1 answer
Imprint | Privacy Policy
...