Binary decision diagrams (bdds) are space-efficient encodings of boolean expressions or dynamic truth tables, used in eg. model checking. this is the runtime package for programs that use the buddy library.