CMU CS 15414 - Binary Decision Diagrams Part 1 (53 pages)
Previewing pages 1, 2, 3, 4, 24, 25, 26, 50, 51, 52, 53 of 53 page document View the full content.Binary Decision Diagrams Part 1
Previewing pages 1, 2, 3, 4, 24, 25, 26, 50, 51, 52, 53 of actual document.
View the full content.View Full Document
Binary Decision Diagrams Part 1
0
0
49 views
- Pages:
- 53
- School:
- Carnegie Mellon University
- Course:
- Cs 15414 - Bug Catching: Automated Program Verification and Testing
Unformatted text preview:
Binary Decision Diagrams Part 1 15 414 Bug Catching Automated Program Verification and Testing Sagar Chaki September 12 2011 2011 Carnegie Mellon University BDDs in a nutshell Typically mean Reduced Ordered Binary Decision Diagrams ROBDDs Canonical representation of Boolean formulas Often substantially more compact than a traditional normal form Can be manipulated very efficiently Conjunction Disjunction Negation Existential Quantification R E Bryant Graph based algorithms for boolean function manipulation IEEE Transactions on Computers C 35 8 1986 Binary Decision Diagrams Part 1 Sagar Chaki Sep 12 2011 2011 Carnegie Mellon University 2 Running Example Comparator a1 a2 b1 b2 Comparator f 1 a1 b1 a2 b2 Binary Decision Diagrams Part 1 Sagar Chaki Sep 12 2011 2011 Carnegie Mellon University 3 Conjunctive Normal Form f a1 b1 a1 b1 b1 a1 a2 b2 a2 b2 b2 a2 a1 b1 b1 a1 a2 b2 b2 a2 b1 a1 a1 b1 a2 b2 b2 a2 Not Canonical Binary Decision Diagrams Part 1 Sagar Chaki Sep 12 2011 2011 Carnegie Mellon University 4 Truth Table 1 a1 b1 a2 b2 f 0 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 0 1 1 1 0 1 0 0 0 0 1 0 1 0 0 1 1 0 0 0 1 1 1 0 1 0 0 0 0 1 0 0 1 0 1 0 1 0 0 1 0 1 1 0 1 1 0 0 1 1 1 0 1 0 1 1 1 0 0 1 1 1 1 1 Still Not Canonical Binary Decision Diagrams Part 1 Sagar Chaki Sep 12 2011 2011 Carnegie Mellon University 5 Truth Table 2 a1 a2 b1 b2 f 0 0 0 0 1 0 0 0 1 0 0 0 1 0 0 0 0 1 1 0 0 1 0 0 0 0 1 0 1 1 0 1 1 0 0 0 1 1 1 0 1 0 0 0 0 1 0 0 1 0 1 0 1 0 1 1 0 1 1 0 1 1 0 0 0 1 1 0 1 0 1 1 1 0 0 1 1 1 1 1 Canonical if you fix variable order Binary Decision Diagrams Part 1 But always exponential in of variables Let s fix Sagartry Chaki to Sep 12 2011this 2011 Carnegie Mellon University 6 Representing a Truth Table using a Graph a1 0 b1 b1 0 a2 a2 0 1 a2 1 b2 0 a2 b2 1 0 0 0 b2 b2 b2 b2 b2 b2 1 1 0 0 0 0 0 0 0 0 1 0 0 1 Binary Decision Tree in this case ordered Binary Decision Diagrams Part 1 Sagar Chaki Sep 12 2011 2011 Carnegie Mellon University 7 Binary Decision Tree Formal Definition Balanced
View Full Document