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
66 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
-
Software Verification using Predicate Abstraction and Iterative Refinement: Part 1
36 pages
-
47 pages
-
14 pages
-
38 pages
-
53 pages
-
42 pages
-
68 pages
-
34 pages
-
Partial Order Reduction (Recitation)
20 pages
-
33 pages
-
59 pages
-
36 pages
-
23 pages
-
46 pages
-
48 pages
-
Introduction to JavaPathfinder
40 pages
-
46 pages
-
Lecture 1: Propositional Logic
22 pages
-
75 pages
-
4 pages
-
28 pages
-
Introduction to JavaPathfinder
18 pages
-
Chaff: Engineering an Efficient SAT Solver
38 pages
-
59 pages
-
39 pages
-
Order Theory, Galois Connections and Abstract Interpretation
81 pages
-
23 pages
-
68 pages
-
82 pages
-
Automated Program Verification and Testing
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
Study Guide: Midterm 2
Unlocking...