From the lecture notes
- Section 9 Exercises: 41
- Section 10 Exercises: 43, 45
- Section 11 Exercises: 49, 50
- Section 12 Exercises: 51
Exam questions
- 2009/6/7
- 2012/6/6 (in part (a) only use tableau calculus, but still write about the differences of each method.)
Implementation
This is bonus question, don’t do it if you don’t feel like it.
Write a program to convert a propositional formula to its BDD representation.
A tree data structure suffices as output, but once you have that it shouldn’t be too difficult to output a file in DOT language, which gives you a nice pictorial representation.