Evaluating #SAT solvers on industrial feature models
Chico Sundermann, Thomas Thüm, Ina Schaefer
Abstract
Configurable systems are widely used for families of products that share multiple configuration options. These systems often induce a large configuration space. Handling the variability of such a system is difficult without being able to measure its complexity. Several methods depend on computing the number of valid configurations, such as estimating the effort of an update or effectively reducing the variability of a system. In many cases, it is possible to map a configurable system to propositional logic. Therefore, we use #SAT in order to evaluate variability of such systems. A #SAT solver computes the number of valid assignments of a propositional formula. However, this problem is even harder than SAT. The main contribution of our work is an investigation of the scalability of off-the-shelf #SAT solvers on industrial feature models. Additionally, we examine the correlation between size of a system and the runtime of a solver computing the number of valid configurations. In this paper, we empirically evaluate nine publicly available #SAT solvers on 127 industrial feature models. Our results indicate that current solvers master a majority of the evaluated systems. However, there are large models, for which none of the evaluated solvers scales. Nevertheless, there are even larger and more complex systems for which the solvers scale.