Transforming numerical feature models into propositional formulas and the universal variability language

Abstract

Real-world Software Product Lines (SPLs) need Numerical Feature Models (NFMs) whose features have not only boolean values that satisfy boolean constraints but also have numeric attributes that satisfy arithmetic constraints. An essential operation on NFMs finds near-optimal performing products, which requires counting the number of SPL products. Typical constraint satisfaction solvers perform poorly on counting and sampling. Nemo (Numbers, features, models) is a tool that supports NFMs by bit-blasting, the technique that encodes arithmetic expressions as boolean clauses. The newest version, Nemo2, translates NFMs to propositional formulas and the Universal Variability Language (UVL). By doing so, products can be counted efficiently by #SAT and Binary Decision Tree solvers, enabling finding near-optimal products. This article evaluates Nemo2 with a large set of synthetic and colossal real-world NFMs, including complex arithmetic constraints and counting and sampling experiments. We empirically demonstrate the viability of Nemo2 when counting and sampling large and complex SPLs.