Domain-specific variable ordering for compiling binary decision diagrams from feature models

Abstract

Feature-model analysis often involves the use of Boolean satisfiability (SAT) solvers. An alternative approach is the use of binary decision diagrams (BDD), which allow SAT operations to be performed efficiently. The variable ordering of BDDs can have a significant impact on their efficiency, as it affects their size. As identifying optimal variable orderings is a NP-complete problem, heuristics are employed to produce at least sufficient orderings. For feature models, most approaches are not usable, do not scale well to current realworld feature models, do not yield reliable results, or require hierarchical knowledge of feature models. Since feature models are often extracted from different formats and are usually represented in conjunctive normal form (CNF), there is often a lack of structural knowledge at the outset. In this work, we aim to preprocess CNFs derived from feature models in order to recover different structures such as XORs derived from alternative groups or influential variables, such as the independent support. We integrate this knowledge into the current state-of-the-art variable ordering heuristic FORCE in order to enable the exploitation of structural characteristics of feature models without requiring additional hierarchical information. We evaluate the benefits of this approach for compiling BDDs from feature models on up to 103 real-world feature models. Our results demonstrate that exploiting XORs on feature models reduces the spans for the resulting variable orderings as well as significantly decreases the runtimes of FORCE. This extends to the compilation of BDDs, where we have successfully compiled BDDs for models such as automotive02_V4 within 100 seconds. Overall, our work introduces a promising method for compiling BDDs from feature models using structural characteristics without requiring any input other than a CNF representation.