Towards Deterministic Compilation of Binary Decision Diagrams From Feature Models

Compiling binary decision diagrams (BDD) from feature models is a challenging task whose outcome and performance depends on many interconnected factors. As almost all of these factors trace back to the BDD’s variable order, finding suitable orders is paramount for compilation success. In addition to cross-tree constraints, Alternative groups in feature models pose a challenge for variable ordering as separating group variables in the order can lead to duplication of large parts of the BDD. Previous approaches only scale to under-constrained models and require knowledge of the feature hierarchy. We address both shortcomings with a novel deterministic variable-ordering heuristic that detects Alternative groups in Boolean formulas and exploits them for variable ordering using the well-known FORCE heuristic in a divide-and-conquer approach. Our evaluation shows that this heuristic, together with our compilation strategy, scales to many models for which BDDs could not be compiled previously. Thereby, this work resolves SPLC’s knowledge compilation challenge for an important subset of real-world models.