## 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.