Applications of #SAT Solvers on Feature Models
Chico Sundermann, Michael Nieke, Paul Maximilian Bittner, Tobias Heß, Thomas Thüm, Ina Schaefer
Abstract
Product lines are ubiquitous for managing variable systems. The variability of a product line is typically described in terms of a feature model. Analyzing a feature model gives insight into various aspects, such as the validity of a configuration of features. Several analyses have been considered that require computing the number of valid configurations which proves highly inefficient when using regular SAT solvers. A #SAT solver computes the number of satisfying variable assignments of a propositional formula and is specifically optimized for the aforementioned analyses. In this work, we summarize and unify the state-of-the-art on #SAT-based feature-model analyses and propose a variety of new #SAT-based analyses. We provide an exhaustive catalogue for applications of #SAT for feature models serving as a reference for researchers and practitioners. Furthermore, we show that all these 21 applications are based on only three different #SAT queries. Thus, future research can focus on providing solutions and optimizations for those three queries to accelerate #SAT-based applications.