# 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 Full Document

# Binary Decision Diagrams Part 1

Previewing pages 1, 2, 3, 4, 24, 25, 26, 50, 51, 52, 53 of actual document.

View Full Document
View Full Document

## Binary Decision Diagrams Part 1

49 views

Pages:
53
School:
Carnegie Mellon University
Course:
Cs 15414 - Bug Catching: Automated Program Verification and Testing
##### Bug Catching: Automated Program Verification and Testing Documents
• 36 pages

• 47 pages

• 14 pages

• 38 pages

• 53 pages

• 42 pages

• 68 pages

• 34 pages

• 20 pages

• 33 pages

• 59 pages

• 36 pages

• 23 pages

• 46 pages

• 48 pages

• 40 pages

• 46 pages

• 22 pages

• 75 pages

• 4 pages

• 28 pages

• 18 pages

• 38 pages

• 59 pages

• 39 pages

• 81 pages

• 23 pages

• 68 pages

• 82 pages

• 37 pages

• 39 pages

• 39 pages

• 37 pages

• 54 pages

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

Unlocking...