Binary decision diagram

Summary

A binary decision diagram is a directed acyclic graph that represents a Boolean function. To evaluate the function, start at the root and read the variable named at each node. Follow the edge for its value until a terminal node $0$ or $1$ is reached. Fix the order in which the variables are tested and merge redundant nodes. Then the reduced ordered diagram of a function is unique, so equality of functions becomes equality of diagrams. This makes binary decision diagrams a basic tool in hardware verification and model checking.