Exploiting d-DNNFs for Repetitive Counting Queries on Feature Models

TL;DR

This paper introduces a novel approach that leverages d-DNNFs to efficiently perform repetitive counting queries on feature models, significantly reducing computation time compared to traditional #SAT-based methods.

Contribution

It is the first to utilize reusing d-DNNFs for efficient repetitive counting queries on feature models, enhancing performance and scalability.

Findings

Up to 8,300 times faster than #SAT solvers

Reduces runtimes from days to minutes

Saves 99.99% CPU time

Abstract

Feature models are commonly used to specify the valid configurations of a product line. In industry, feature models are often complex due to a large number of features and constraints. Thus, a multitude of automated analyses have been proposed. Many of those rely on computing the number of valid configurations which typically depends on solving a #SAT problem, a computationally expensive operation. Further, most counting-based analyses require numerous #SAT computations on the same feature model. In particular, many analyses depend on multiple computations for evaluating the number of valid configurations that include certain features or conform to partial configurations. Instead of using expensive repetitive computations on highly similar formulas, we aim to improve the performance by reusing knowledge between these computations. In this work, we are the first to propose reusing d-DNNFs for performing efficient repetitive queries on features and partial configurations. Our empirical evaluation shows that our approach is up-to 8,300 times faster (99.99\% CPU-time saved) than the state of the art of repetitively invoking #SAT solvers. Applying our tool ddnnife reduces runtimes from days to minutes compared to using #SAT solvers.