Binary Decision Diagrams Part 2© 2011 Carnegie Mellon University15-414 Bug Catching: Automated Program Verification and TestingSagar ChakiSeptember 14, 2011BDDs RecapTypically mean Reduced Ordered Binary Decision Diagrams (ROBDDs)• Can be viewed as reduced forms of Ordered Binary Decision Trees• Obtained by eliminating duplicate nodes and redundant nodes• Often substantially smaller than the OBDTCanonical representation of Boolean formulas•Unlike other normal forms like CNF and DNF2Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•Unlike other normal forms like CNF and DNFSize of BDD depends critically on variable orderingIn practice, BDDs are built up from their components• Via (efficient) Boolean operations• Dynamic variable ordering used to manage BDD sizeRunning Example: ComparatorComparatora1a2b1b23Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University(A) f = 1 ⇔⇔⇔⇔ a1= b1ÆÆÆÆ a2= b2(B) f = 1 ⇔⇔⇔⇔ a1= b1ÇÇÇÇ a2= b2Conjunctive Normal Form(¬ b1Ç a1) Æ (¬ a1Ç b1) Æ (¬ a2Ç b2) Æ (¬ b2Ç a2)(b1Ç a1) Æ (¬ a1Ç ¬ b1) Æ (¬ a2Ç b2) Æ (¬ b2Ç a2)4Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University(¬ a1Ç b1) Æ (¬ b1Ç a1) Æ (¬ a2Ç b2) Æ (¬ b2Ç a2)(¬ a1Ç b1) Æ (¬ b1Ç a1) Æ (¬ a2Ç ¬ b2) Æ (b2Ç a2)Truth TableRow# a1b1a2b2f0 0 0 0 0 01 0 0 0 1 12 0 0 1 0 03 0 0 1 1 14 0 1 0 0 05 0 1 0 1 16 0 1 1 0 07 0 1 1 1 08100005Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University8100009 1 0 0 1 110 1 0 1 0 111 1 0 1 1 012 1 1 0 0 113 1 1 0 1 014 1 1 1 0 015 1 1 1 1 0Representing a Truth Table using a Grapha1b1b1a2a2a2b26Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universitya2a2b1b2b2b2a2b2b2b2a2a2Representing a Truth Table using a Grapha1b1b1a2a2a2a27Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universitya2a2b2b21 0 1 1b2b21 0 0 0a2a2b2b21 0 0 0b2b20 0 0 0OBDT to ROBDDa1b1b1a2a2Which pairs are isomorphic?(1) {A,B} and {C,D}(2) {A,C} and {B,D}(3) {A,D} and {B,C}8Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityb2b210b2b2A BC DOBDT to ROBDDa1b1b1a2Is this a ROBDD?(1) YES(2) NO9Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityb210b2OBDT to ROBDDa1b1b1a2What function does X represent?(1) a2= b2(2) a2= (¬¬¬¬ b2)(3) a2⇒⇒⇒⇒ b2(4) a2⊕⊕⊕⊕ b2(5) ¬(a2⊕⊕⊕⊕ b2)(6) (a2ÆÆÆÆ b2) ÇÇÇÇ (¬¬¬¬ a2ÆÆÆÆ ¬¬¬¬ b2)X1,5,610Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityb210b2ROBDD (a.k.a. BDD) SummaryIf BDD(f1) and BDD(f2) are isomorphic then:1. f1= f22. f1and f2have the same variables3. BDD(f1) and BDD(f2) have the same variable orderingIf BDD(f) is the leaf node “1” then f is: 1.Satisfiable11Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University1.Satisfiable2. Unsatisfiable3. ValidROBDD and variable orderinga1a2a2b1b1b1b1Is this a ROBDD?(1) YES(2) NO12Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityb21 0b2b2ROBDD and variable orderinga1a2a2b1b1b1b1Is this a ROBDD?(1) YES(2) NO13Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityb21 0b2ROBDD and variable orderingThere exists a function whose BDD grows polynomially in the number of variables for some ordering and exponentially for others?• TRUEThere exists a function whose BDD grows exponentially for all variable orderings?•TRUE14Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University•TRUEThere exists a function whose BDD grows linearly for all variable orderings?• TRUEBDD OperationsTrue : BDD(TRUE)False: BDD(FALSE)Var : v a BDD(v)15Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityNot : BDD(f) a BDD(¬f)And : BDD(f1) × BDD(f2) a BDD(f1Æ f2)Or : BDD(f1) × BDD(f2) a BDD(f1Ç f2)Exist : BDD(f) × v a BDD(∃ v. f)Basic BDD OperationsTrue False1016Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityVar(v)10vBDD Operations: Not1 001vOOOO(1)OOOO(1)17Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University10BDD Operations: Not1 001vOOOO(1)OOOO(1)18Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University01Swap “0” and “1”OOOO(n)BDD Operations: AndvWhat formula does this represent?What formula does this represent?Suppose this is the BDD for f 19Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityBDD Operations: Andvfv=0Suppose this is the BDD for f fv=120Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityfv=0and fv=1 are known as the co-factors of f w.r.t. v f = (X Æ fv=0) ÇÇÇÇ (Y ÆÆÆÆ fv=1)BDD Operations: Andvfv=0Suppose this is the BDD for f fv=121Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityfv=0and fv=1 are known as the co-factors of f w.r.t. vf = (¬ v Æ fv=0) ÇÇÇÇ (v ÆÆÆÆ fv=1)BDD Operations: And (Simple Cases)And (f, ) = 0 0And (f, ) = 1f22Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon UniversityAnd ( ,f ) = 1fAnd ( ,f ) = 00BDD Operations: And (Complex Case)v1v2ÆÆÆÆ23Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityf1g1f2g21(¬ v1Æ f1) ÇÇÇÇ (v1ÆÆÆÆ g1)2(¬ v2Æ f2) ÇÇÇÇ (v2ÆÆÆÆ g2)ÆÆÆÆÆÆÆÆBDD Operations: And (Complex Case 1)v1v1ÆÆÆÆv1= v224Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon Universityf1g1f2g21(¬ v1Æ f1) ÇÇÇÇ (v1ÆÆÆÆ g1)1(¬ v1Æ f2) ÇÇÇÇ (v1ÆÆÆÆ g2)ÆÆÆÆÆÆÆÆBDD Operations: And (Complex Case 1)v1= v225Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011 Carnegie Mellon University1(¬ v1Æ f1) ÇÇÇÇ (v1ÆÆÆÆ g1)1(¬ v1Æ f2) ÇÇÇÇ (v1ÆÆÆÆ g2)ÆÆÆÆ1(¬ v1Æ X) ÇÇÇÇ (v1ÆÆÆÆ Y)BDD Operations: And (Complex Case 1)v1= v2Compute recursivelyCompute recursively26Binary Decision Diagrams – Part 2Sagar Chaki, Sep 14, 2011© 2011