Slide 1BDDs in a nutshellRunning Example: ComparatorConjunctive Normal FormTruth Table (1)Truth Table (2)Representing a Truth Table using a GraphBinary Decision Tree: Formal DefinitionBinary Decision TreeBinary Decision TreeBinary Decision TreeBinary Decision TreeBinary Decision TreeBinary Decision Tree (BDT)Reduced Ordered BDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDOBDT to ROBDDROBDD (a.k.a. BDD) SummaryROBDD (a.k.a. BDD) SummaryROBDD (a.k.a. BDD) SummaryROBDD (a.k.a. BDD) SummaryROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingROBDD and variable orderingNext ClassQuestions?© 2011 Carnegie Mellon UniversityBinary Decision Diagrams Part 115-414 Bug Catching: Automated Program Verification and TestingSagar ChakiSeptember 12, 20112Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBDDs in a nutshellTypically mean Reduced Ordered Binary Decision Diagrams (ROBDDs)Canonical representation of Boolean formulasOften substantially more compact than a traditional normal formCan be manipulated very efficiently•Conjunction, Disjunction, Negation, Existential QuantificationR. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.3Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityRunning Example: ComparatorComparatora1a2b1b2f = 1 , a1 = b1 Æ a2 = b24Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityConjunctive Normal Form(: a1 Ç b1 ) Æ (: b1 Ç a1) Æ (: a2 Ç b2 ) Æ (: b2 Ç a2)a1 = b1 Æ a2 = b2a1 ) b1 Æ b1 ) a1 Æ a2 ) b2 Æ b2 ) a2(: b1 Ç a1 ) Æ (: a1 Ç b1) Æ (: a2 Ç b2 ) Æ (: b2 Ç a2)Not Canonicalf5Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityTruth Table (1)a1b1a2b2f0 0 0 0 10 0 0 1 00 0 1 0 00 0 1 1 10 1 0 0 00 1 0 1 00 1 1 0 00 1 1 1 01 0 0 0 01 0 0 1 01 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 1Still Not Canonical6Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityTruth Table (2)a1a2b1b2f0 0 0 0 10 0 0 1 00 0 1 0 00 0 1 1 00 1 0 0 00 1 0 1 10 1 1 0 00 1 1 1 01 0 0 0 01 0 0 1 01 0 1 0 11 0 1 1 01 1 0 0 01 1 0 1 01 1 1 0 01 1 1 1 1Canonical if you fix variable order.But always exponential in # of variables. Let’s try to fix this.7Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityRepresenting a Truth Table using a Grapha1b1b1a2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 10000 1110Binary Decision Tree (in this case ordered)8Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Tree: Formal DefinitionBalanced binary tree. Length of each path = # of variablesLeaf nodes labeled with either 0 or 1Internal node v labeled with a Boolean variable var(v)•Every node on a path labeled with a different variableInternal node v has two children: low(v) and high(v)Each path corresponds to a (partial) truth assignment to variables•Assign 0 to var(v) if low(v) is in the path, and 1 if high(v) is in the pathValue of a leaf is determined by:•Constructing the truth assignment for the path leading to it from the root•Looking up the truth table with this truth assignment9Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Treea1b1b1a2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 10000 1110vlow(v)high(v)var(v) = a110Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Treea1b1a2b20010The truth assignment corresponding to the path to this leaf is:a1 = ? b1 = ? a2 = ? b2 = ?11Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Treea1b1a2b20010The truth assignment corresponding to the path to this leaf is:a1 = 0 b1 = 0 a2 = 1 b2 = 0a1b1a2b2f0 0 0 0 10 0 0 1 00 0 1 0 00 0 1 1 10 1 0 0 00 1 0 1 00 1 1 0 00 1 1 1 01 0 0 0 01 0 0 1 01 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 112Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Treea1b1a2b20010The truth assignment corresponding to the path to this leaf is:a1 = 0 b1 = 0 a2 = 1 b2 = 0a1b1a2b2f0 0 0 0 10 0 0 1 00 0 1 0 00 0 1 1 10 1 0 0 00 1 0 1 00 1 1 0 00 1 1 1 01 0 0 0 01 0 0 1 01 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 113Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Treea1b1a2b200010The truth assignment corresponding to the path to this leaf is:a1 = 0 b1 = 0 a2 = 1 b2 = 0a1b1a2b2f0 0 0 0 10 0 0 1 00 0 1 0 00 0 1 1 10 1 0 0 00 1 0 1 00 1 1 0 00 1 1 1 01 0 0 0 01 0 0 1 01 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 114Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityBinary Decision Tree (BDT)a1b1b1a2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 10000 1110Canonical if you fix variable order (i.e., use ordered BDT)But still exponential in # of variables. Let’s try to fix this.15Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityReduced Ordered BDDConceptually, a ROBDD is obtained from an ordered BDT (OBDT) by eliminating redundant sub-diagrams and nodesStart with OBDT and repeatedly apply the following two operations as long as possible:1. Eliminate duplicate sub-diagrams. Keep a single copy. Redirect edges into the eliminated duplicates into this single copy.2. Eliminate redundant nodes. Whenever low(v) = high(v), remove v and redirect edges into v to low(v).•Why does this terminate?ROBDD is often exponentially smaller than the corresponding OBDT16Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityOBDT to ROBDDa1b1b1a2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 117Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityOBDT to