A binary decision diagram (BDD) is a popular data structure for representing a set of truth-value assignments for a fixed finite set of Boolean variables. The goal of this thesis is to map and evaluate the existing techniques for underapproximation of BDDs. More precisely, the student will design an algorithm that, for a given BDD and a node limit, computes the maximal size of an assignment set that is

• a subset of the assignment set represented by the BDD and 
• can be represented by a BDD with a number of nodes less than or equal to the given limit without changing the variable order. 

These sizes represent the optimal underapproximation of a given BDD within the given node limit. 
Further, the student will describe existing algorithms for BDD underapproximation implemented in CUDD, illustrate them on suitable examples, evaluate them on a set of BDDs from practical sources (e.g., the SMT solver Q3B), and on a set of smaller BDDs for which optimal value computation is feasible. 

Further, the student will try to introduce an underapproximation method that performs better in some cases where the current techniques perform significantly worse than the optimal one.

The created code will be available as a part of the thesis under a suitable permissive license.