ROBDDs Construction

Question

Hi,

Is it possible to construct ROBDD direct from truth table? Is it somehow possible to avoid using SNF to construct ROBDD? as it can take a lot of time to calculate for two-variable orderings. The second thing is that can we simplify the expression before computing SNF? if yes then two simplified expressions are returning different Shanon forms and will lead to different ROBDDs. For example !(d -> (a & c)) <->b is logically equivalent to (d & !a | !c) <-> b but I am getting two different SNF's from the tool.

Answer 1

Basically yes. Each satisfying assignment (line ending with the result 1 in the truth table) corresponds to a path from the root node to the 1-leaf. If you add path after path (while not adding nodes that already exist), you get an OBDD. In order to get an ROBDD, you need to delete redundant structures and double nodes with double edges.

Edit: When adding paths, do that starting from the 1-leaf.