Comparing Solver Representations for Analyzing Cardinality-Based Feature Models

Abstract

The variability of product lines can exceed purely Boolean configuration spaces. Cardinality-based Feature Models (CFMs) are employed to model multi-instantiation of features along with individually configurable subtrees. Due to the added complexity, the analysis of CFMs cannot be done with state-of-the-art, SAT-based tooling for analyzing Boolean Feature Models (FMs). Analyses on FMs include checking for satisfying configurations, dead features, false optional features, and whether specific configurations are valid according to the FM. In this work, we compare different solver encodings to enable analysis for CFMs. First, we generalize the analyses on Boolean FMs to the notion of cardinalities and the new anomalies that can occur. Second, we present three different mathematical encodings of CFMs for automated reasoning using solvers. Third, we implement the encoding for ILP, SMT, and CSP solvers. We evaluate the feasibility and performance of our encodings on current ILP, SMT, and CSP solvers. Our evaluation shows that our encoding for CSP solvers enables all common analyses with the best performance among the compared encodings and solvers.