Binary Decision Diagram (BDD)

A Binary Decision Diagram (BDD) is a data structure that represents the complete set of valid configurations of a product family as a graph that can be navigated efficiently — provided the product model is not too large or too densely constrained. In variant management and product line engineering, BDDs are valued for operations that go beyond checking whether a single configuration is valid — in particular, counting how many valid configurations exist, and identifying which product options are unreachable under the current rule set.

The form used in practice is the Reduced Ordered BDD (ROBDD): a BDD in which a fixed variable ordering is applied and two reduction rules eliminate redundant nodes. For a given variable ordering, every Boolean formula has exactly one ROBDD — a property called canonicity — which makes comparing two constraint models straightforward.

What BDDs are used for in variant management

The constraint model of a product family — the rules governing which option combinations are valid — can be encoded as a Boolean formula. A BDD turns this formula into a graph where each path from root to leaf corresponds to a set of valid or invalid configurations.

Once the BDD is built, certain analysis operations that would otherwise require exhaustive search become tractable:

• Configuration counting — how many valid configurations does the product family have? Counting is a computationally hard problem for any approach; BDDs make it tractable once the diagram is constructed, at the cost of potentially exponential construction time. SAT-based model counters (sharpSAT, d4, GANAK) offer an alternative route to the same result.
• Dead feature detection — which product options appear in no valid configuration? Dead options often indicate an error in the constraint model — a rule was added that inadvertently makes a valid choice unreachable.
• Configuration enumeration — generating the full set of valid configurations, or a representative sample, for downstream analysis.

Feature model tools such as FeatureIDE support BDD-based analysis (via the JavaBDD library) alongside SAT-based alternatives; which backend is used depends on the operation and the model size.

In a CPQ tool, BDD-based analysis typically surfaces in offline reports — for example, when the system warns that a certain option is never selectable under the current rule set — rather than in the real-time configuration dialog itself.

BDDs and SAT solvers

BDDs and SAT solvers SAT Solver (ˌes-ˌā-ˈtē ˈsäl-vər) n. A SAT solver determines whether a Boolean formula is satisfiable — used in variant management to validate configurations and navigate large variant spaces. address similar problems from different angles. For practitioners choosing between them, the distinction is roughly this:

• SAT solvers are the right tool for checking whether a single specific configuration is valid — which is what a product configurator needs in real time, every time a customer makes a selection. They scale well to large numbers of options and dense rule sets.
• BDDs are more useful when the goal is to analyze the entire configuration space — counting all valid configurations, finding all dead options — rather than validating individual selections.

BDD size can grow exponentially depending on how variables are ordered in the diagram. For large, densely constrained product models, this can make BDD construction infeasible, while SAT solvers continue to work well. Hybrid approaches — SAT for real-time validation, BDDs for offline analysis — are standard in product line engineering research.

Note: checking whether any valid configuration exists at all (void product line detection) is a plain satisfiability check. SAT solvers handle this efficiently and are generally preferred over BDDs for this specific task.

Frequently asked questions