Tailoring binary decision diagram compilation for feature models

Clemens DubslaffClemens Dubslaff, Nils HusungNils Husung, Nikolai KäferNikolai Käfer

ISSN: 0164-1212
DOI Link

Clemens Dubslaff, Nils Husung, Nikolai Käfer
Tailoring binary decision diagram compilation for feature models
Journal of Systems and Software, 231, 2025

Details
Bibtex

KurzfassungAbstract
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.
Projekt:Project: CPEC
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{DHK2025,
  author  = {Clemens Dubslaff and Nils Husung and Nikolai K{\"{a}}fer},
  title   = {Tailoring binary decision diagram compilation for feature models},
  journal = {Journal of Systems and Software},
  volume  = {231},
  year    = {2025},
  doi     = {10.1016/j.jss.2025.112566}
}