Tailoring binary decision diagram compilation for feature models

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.