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.
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 the full content.
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

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

Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Binary Decision Diagrams Part 1 and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Binary Decision Diagrams Part 1 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?