BDD (binary decision diagram)
Beginner
A compact diagram that stands for a yes-or-no rule. It lets tools reason about huge numbers of cases at once.
Novice
Binary decision diagram: a compact graph that represents a logic function as a chain of yes/no decisions on its inputs, so tools can reason about very large numbers of input combinations at once.
Expert
For a fixed order of the input variables the graph is unique, so checking two functions for equality is a pointer comparison. Its size depends heavily on that order, and for some functions, multipliers among them, it is exponential whatever the order.