Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Binary decision diagrams (BDD) are data structures that represent Boolean functions. Two of the most fundamental properties of BDDs are the abilities to solve the satisfiability problem (SAT) and count the number of solutions for the satisfi- ability problem (#SAT) e ciently. Additionally, the Boolean function NOT can be applied in constant time and the Boolean functions AND and OR can be applied in polynomial time. While SAT can be solved in constant time, #SAT can be solved in linear time, with respect to the number of nodes in the BDD. Solving SAT and #SAT e ciently is important for many real world applications, such as product-line anal- ysis and circuit analysis. Currently, there exist several libraries to generate BDDs from Boolean functions, the most widespread being BuDDy and CUDD, both whom are not maintained anymore by their creators. Both BuDDy and CUDD require expert knowledge about BDDs to use and do not support parallelized execution. There ex- ist libraries for parallelized BDD execution, like Sylvan, but they are less powerful than BuDDy and CUDD. In this thesis, we address the shortcomings by providing an architecture for a BDD library with not only parallelization in mind, but addi- tionally, we want the architecture to be modular so the different algorithms used for the construction of the BDD can be exchanged to measure runtime impacts of different implementations. We also give high priority to maintainability and ease of use. As a result of the design process, we provide an architecture that meets the specified points of parallelism, extensibility, maintainability and ease of use, ensured by software design patterns, like the facade pattern and the pipes-and- filters pattern. Furthermore, we provide a proof-of-concept implementation as a minimal viable product of the described architecture in the Rust programming lan- guage which can construct BDDs using parallelism, solve SAT and #SAT and provide manipulation through Boolean functions.