Binary Decision Diagrams (BDDs) are widely used to efficiently encode and visually represent Boolean functions. BDDs use recursive algorithms to apply logical operators, which makes the manipulation and reduction of Boolean functions more efficient. BDDs can also be used to analyze the behavior of a Boolean function due to the branching structure of the BDD, which shows possible decisions for variables. Knowing the ‘importance’ of these decisions can give insight into the impact of this variable assignment to the final result of the Boolean function. This leads to our main goal:

Make decisions in Binary Decision Diagrams more comprehensible.

To this end, we aim to adapt a known importance method to define variable and decision importance in BDDs, effectively compute these values, and then visualize these results. First, we provide background information about Boolean functions and Binary Decision Diagrams, after which we discuss Shapley values which are a known method for computing the importance of features. Next, we adapt the Shapley values to be applicable to Boolean functions and define our notions of importance. Using existing methods, we prove lemmas to derive a method to compute our notion of importance for BDDs. Based on these computations, we then create an efficient algorithm that computes the importance values for each node in a BDD, using memoization. We discuss the implementation of the algorithm, where we use Python and OxiDD, where CNF files are used as input. The results of the algorithm are analyzed using plots, and also compared to the naive Shapley method for correctness and efficiency. Lastly, we show a new method for visualizing the importance of variables and decisions in a BDD, where we draw inspiration from SHAP and known visualization approaches.