A Fast Counting-Free Algorithm for Computing Atomic Sets in Feature Models

TL;DR

This paper tackles the problem of computing atomic sets in feature models, a task important for simplifying configurations without changing satisfiability. It introduces GnT, a counting-free algorithm that relies exclusively on SAT solving to identify atomic sets, guided by SAT-certificates and generate-and-test steps. Empirical results show GnT outperforms state-of-the-art tools by at least an order of magnitude on most benchmarks and scales to challenging models like Linux kernel variants; atomic-set elimination (ASE) also materially reduces CNF size and synergizes with existing preprocessors. The findings demonstrate the practical viability of SAT-based atomic-set computation and establish ASE as a promising preprocessing technique for scaling feature-model analyses and knowledge compilation workflows.

Abstract

In the context of product-line engineering and feature models, atomic sets are sets of features that must always be selected together in order for a configuration to be valid. For many analyses and applications, these features may be condensed into one feature, without affecting, for instance, satisfiability, model counting, sampling, or knowledge compilation. However, the performance of current approaches tends to be insufficient in practice. This is especially true but not limited to approaches based on model counting. In this work, we present a counting-free algorithm for computing atomic sets that only relies on SAT solving. Our evaluation shows that it scales with ease to hard real-world systems and even succeeds for a contemporary version of the Linux kernel.

Figures (2)

• Figure 1: Example of a Feature Model
• Figure 2: Boxplot of Tool Performances