Enabling SAT-Based Analysis of Cardinality-Based Feature Models By Unfolding

Cardinality-based Feature Models (CFMs) are used to model complex configuration spaces, extending classical FODA Feature Models (FMs) by cardinalities, thereby allowing for multi-instantiation and individual sub-configuration of features. This extension in expressiveness comes at the price of a bigger, more complex configuration space. While there is (mostly SAT-based) analysis tooling for Boolean FMs, CFMs lack extensive tool support due to the more complex encodings and solvers needed to run analyses or perform sampling. In this paper, we inspect the conversion of CFMs to FMs describing the same configuration space. We provide an algorithm to translate all CFM structures to an equivalent FM and investigate its applicability and the characteristics of the resulting Boolean FMs. We find that the unfolding algorithm is feasible, but the resulting FMs massively grow in size and predominantly consist of auxiliary variables encoding the multiplicity constraints.