The compilation of feature models into binary decision diagrams (BDDs) is a major challenge in the area of configurable systems analysis. For many large-scale feature models such as the variants of the prominent Linux product line, BDDs could not yet be obtained due to exceeding state-of-the-art compilation capabilities. Until now, BDD compilation has been mainly considered on standard settings of existing BDD tools, barely exploiting advanced techniques or tuning parameters. In this article, we conduct a comprehensive study on how to configure various techniques from the literature and thus improve compilation performance for feature models given in conjunctive normal form. Specifically, we evaluate preprocessing for satisfiability solving (SAT), variable and clause ordering heuristics, as well as non-standard and multi-threaded BDD construction schemes. Our experiments on recent feature models demonstrate that BDD compilation of feature models greatly benefits from these techniques. We show that our methods enable BDD compilations of many large-scale feature models within seconds, including the whole ECOS feature model collection for which a compilation was previously infeasible.

Abstract Decision diagrams (DDs) are an important data structure in computer science with applications ranging from circuit design and verification to machine learning. Most prominently, binary DDs are commonly used to succinctly represent Boolean functions. Due to the practical importance of DDs, there is an ongoing quest for high-performance software libraries supporting the construction and manipulation of DDs. With OxiDD, we present a new framework for DDs that focuses on safety, concurrency, and modularity. Following a highly modular design we implement OxiDD in Rust, which facilitates the integration of various kinds of DDs such as MTBDDs, ZBDDs, and TDDs, all within safe code also in a concurrent setting. Already in its initial release, OxiDD does not compromise performance, which we show to be on par with or even better than established highly optimized DD libraries.