Glossary
What is a binary decision diagram?
A binary decision diagram (BDD) represents a Boolean function as a graph: each node tests one variable and branches to a LO child (variable false) or a HI child (variable true), ending at the sinks 0 and 1. When variables are tested in a fixed order and redundant nodes are merged, the result is a reduced ordered BDD, and it is canonical: two functions are equal exactly when their BDDs are the same graph.
What you can do with one
Count the solutions of a function, find the best one under weights, combine two functions with AND, OR or XOR, and check equivalence in constant time once built. That made BDDs central to hardware verification after Randal Bryant's 1986 paper. Knuth's §7.1.4 part 1 covers the algorithms, including the BDD base with a unique table and memo cache.
Why variable order matters
The same function can have a tiny BDD under one variable order and an exponentially large one under another. Some functions (like multiplication) are large under every order. Part 2 of §7.1.4 covers finding good orders, sifting, and the ZDD variant for families of sets.
Questions
BDD or SAT solver?
A BDD describes all solutions at once and answers counting and equivalence questions; a SAT solver finds one solution or proves there is none, and scales to much bigger problems when you only need that.