Binary Decision Diagrams Part 1© 2011 Carnegie Mellon University15-414 Bug Catching: Automated Program Verification and TestingSagar ChakiSeptember 12, 2011BDDs in a nutshellTypically mean Reduced Ordered Binary Decision Diagrams (ROBDDs)Canonical representation of Boolean formulasOften substantially more compact than a traditional normal form2Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityCan 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.Running Example: ComparatorComparatora1a2b1b23Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityf = 1 ⇔⇔⇔⇔ a1= b1ÆÆÆÆ a2= b2Conjunctive Normal Forma1= b1ÆÆÆÆ a2= b2a1⇒⇒⇒⇒ b1ÆÆÆÆ b1⇒⇒⇒⇒ a1 ÆÆÆÆ a2⇒⇒⇒⇒ b2ÆÆÆÆ b2⇒⇒⇒⇒ a2f4Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon University(¬ a1Ç b1) Æ (¬ b1Ç a1) Æ (¬ a2Ç b2) Æ (¬ b2Ç a2)(¬ b1Ç a1) Æ (¬ a1Ç b1) Æ (¬ a2Ç b2) Æ (¬ b2Ç a2)Not CanonicalTruth 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 0100005Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon University100001 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 CanonicalTruth 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 0100006Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon University100001 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.Representing a Truth Table using a Grapha1b1b1a2a2a2a2007Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 100 1110Binary Decision Tree (in this case ordered)Binary 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 variable8Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon UniversityInternal 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 assignmentBinary Decision Treea1b1b1a2a2a2a200vlow(v)high(v)var(v) = a19Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 100 1110Binary Decision Treea1b1a20010Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2b210The truth assignment corresponding to the path to this leaf is:a1= ? b1= ? a2= ? b2= ?Binary Decision Treea1b1a200a1b1a2b2f0 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 01001011Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2b210The truth assignment corresponding to the path to this leaf is:a1= 0 b1= 0 a2= 1 b2= 0100101 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 1Binary Decision Treea1b1a200a1b1a2b2f0 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 01001012Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2b210The truth assignment corresponding to the path to this leaf is:a1= 0 b1= 0 a2= 1 b2= 0100101 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 1Binary Decision Treea1b1a200a1b1a2b2f0 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 01001013Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2b2010The truth assignment corresponding to the path to this leaf is:a1= 0 b1= 0 a2= 1 b2= 0100101 0 1 0 01 0 1 1 01 1 0 0 11 1 0 1 01 1 1 0 01 1 1 1 1Binary Decision Tree (BDT)a1b1b1a2a2a2a20014Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universitya2a2b2b21 0 0 1b2b20 0 0 0a2a2b2b20 0 0 0b2b21 0 0 100 1110Canonical if you fix variable order (i.e., use ordered BDT)But still exponential in # of variables. Let’s try to fix this.Reduced 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.15Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityinto 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 OBDTOBDT to ROBDDa1b1b1a2a2a2a216Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityb2b21 0 0 1b2b20 0 0 0b2b20 0 0 0b2b21 0 0 1OBDT to ROBDDa1b1b1a2a2a2a2Duplicate sub-diagram17Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityb2b21 0 0 1b2b20 0 0 0b2b20 0 0 0b2b21 0 0 1diagramOBDT to ROBDDa1b1b1a2a2a2a218Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityb2b21 0 0 1b2b20 0 0b2b20 0 0 0b2b21 0 0 1OBDT to ROBDDa1b1b1a2a2a2a219Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityb2b21 0 0 1b2b20 0 0b2b20 0 0 0b2b21 0 0 1OBDT to ROBDDa1b1b1a2a2a2a220Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityb2b21 0 0 1b2b20 0b2b20 0 0 0b2b21 0 0 1OBDT to ROBDDa1b1b1a2a2a2a221Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon Universityb2b21 0 0 1b2b20 0b2b20 0 0 0b2b21 0 0 1OBDT to ROBDDa1b1b1a2a2a2a222Binary Decision Diagrams – Part 1Sagar Chaki, Sep 12, 2011© 2011 Carnegie Mellon