A performance comparison of contemporary algorithmic approaches for automated analysis operations on feature models

The formalization of variability models (e.g. feature models) is a prerequisite for the automated analysis of these models. The efficient execution of the analysis operations depends on the selection of well-suited solver implementations. Regarding feature models, on the one hand, the formalization with Boolean expressions enables the use of SAT or BDD solvers. On the other hand, feature models can be transformed into a Constraint-Satisfaction Problem (CSP) in order to use CSP solvers for validation. This paper presents a performance comparison regarding nine contemporary high-performance solvers, three for each base problem structure (BDD, CSP, and SAT). Four operations on 90 feature models are run on each solver. The results will in turn clear the way for new improvements regarding the automatic verification of software product lines, since the efficient execution of analysis operations is essential to such automatic verification approaches.