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.

翻译：特征模型通常用于指定产品线的有效配置。在工业实践中，由于特征数量庞大且约束条件众多，特征模型往往结构复杂。因此，研究人员提出了多种自动化分析方法。其中许多方法依赖于计算有效配置的数量，而这通常需要求解#SAT问题——一种计算开销巨大的操作。此外，大多数基于计数的分析需要在同一特征模型上进行多次#SAT计算。具体而言，许多分析需要多次评估包含特定特征或符合部分配置的有效配置数量。我们并非对高度相似的公式进行昂贵的重复计算，而是旨在通过重用这些计算间的知识来提升性能。在本工作中，我们首次提出重用d-DNNF（决定否定正规形式）来高效执行针对特征和部分配置的重复查询。实验评估表明，与重复调用#SAT求解器的现有方法相比，我们的方法速度最高提升8,300倍（节省99.99%的CPU时间）。相较于使用#SAT求解器，应用我们的工具ddnnife可将运行时间从数天缩短至数分钟。