Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs

TL;DR

The paper tackles the scalability gap between expressive feature-model constructs and CNF-based reasoning by introducing a pseudo-Boolean encoding for feature models and a compilation pipeline that converts pseudo-Boolean formulas to Boolean d-DNNFs. It develops detailed encodings for both basic and expressive constructs, along with optimizations and tooling to support the workflow. Empirical results show substantial improvements over CNF-based approaches in encoding and compilation times, particularly for constructs like group cardinalities and numeric attributes, while remaining competitive on basic models. This approach broadens the practical applicability of automated reasoning in product lines by enabling efficient analyses of more expressive feature-modeling constructs.

Abstract

Configurable systems typically consist of reusable assets that have dependencies between each other. To specify such dependencies, feature models are commonly used. As feature models in practice are often complex, automated reasoning is typically employed to analyze the dependencies. Here, the de facto standard is translating the feature model to conjunctive normal form (CNF) to enable employing off-the-shelf tools, such as SAT or #SAT solvers. However, modern feature-modeling dialects often contain constructs, such as cardinality constraints, that are ill-suited for conversion to CNF. This mismatch between the input of reasoning engines and the available feature-modeling dialects limits the applicability of the more expressive constructs. In this work, we shorten this gap between expressive constructs and scalable automated reasoning. Our contribution is twofold: First, we provide a pseudo-Boolean encoding for feature models, which facilitates smaller representations of commonly employed constructs compared to Boolean encoding. Second, we propose a novel method to compile pseudo-Boolean formulas to Boolean d-DNNF. With the compiled d-DNNFs, we can resort to a plethora of efficient analyses already used in feature modeling. Our empirical evaluation shows that our proposal substantially outperforms the state-of-the-art based on CNF inputs for expressive constructs. For every considered dataset representing different feature models and feature-modeling constructs, the feature models can be significantly faster translated to pseudo-Boolean than to CNF. Overall, deriving d-DNNFs from a feature model with the targeted expressive constraints can be substantially accelerated using our pseudo-Boolean approach. Furthermore, our approach is competitive on feature models with only basic constructs.

Figures (8)

• Figure 1: Basic Feature Model
• Figure 2: Feature Model Including Expressive Constructs
• Figure 3: Trace for Exhaustive Pseudo-Boolean DPLL
• Figure 4: d-DNNF Corresponding to Traversal in \ref{['figure:exhaustivepseudo']}
• Figure 5: Comparison of Boolean and Pseudo-Boolean Approach for Compiling Expressive Feature Models to d-DNNF