FMSans: An efficient approach for constraints removal and parallel analysis of feature models

Abstract

Cross-tree constraints help to compact feature models by using arbitrary propositional logic formulas, which efficiently capture interdependencies between features. However, the existence of these constraints increases the complexity of reasoning about feature models, whether we use SAT solvers or compile the model to a binary decision diagram for efficient analyses. Although some works have tried to refactor constraints to eliminate them, they deal only with simple constraints (i.e., requires and excludes) or require introducing an additional set of features, increasing the size and complexity of the resulting feature model. This paper presents an approach that eliminates all the cross-tree constraints in regular boolean feature models, including arbitrary constraints in propositional logic formulas. Our approach for removing constraints consists of splitting the semantics of feature models into orthogonal disjoint feature subtrees, which are then analyzed in parallel to alleviate the exponential blow-up in memory of the resulting feature tree. We propose a codification of the constraints and define and analyze different heuristics for constraints ordering to reduce the complexity of identifying the valid disjoint subtrees when removing constraints.