Analyzing a Feature Model (FM) and reasoning on the corresponding configuration space is a central task in Software Product Line (SPL) engineering. Problems such as deciding the satisfiability of the FM and eliminating inconsistent parts of the FM have been well resolved by translating the FM into a conjunctive normal form (CNF) formula, and then feeding the CNF to a SAT solver. However, this approach has some limits for other important reasoning issues about the FM, such as counting or enumerating configurations. Two mainstream approaches have been investigated in this direction: (i) direct approaches, using tools based on the CNF representation of the FM at hand, or (ii) compilation-based approaches, where the CNF representation of the FM has first been translated into another representation for which the reasoning queries are easier to address. Our contribution is twofold. First, we evaluate how both approaches compare when dealing with common reasoning operations on FM, namely counting configurations, pointing out one or several configurations, sampling configurations, and finding optimal configurations regarding a utility function. Our experimental results show that the compilation-based is efficient enough to possibly compete with the direct approaches and that the cost of translation (i.e., the compilation time) can be balanced when addressing sufficiently many complex reasoning operations on large configuration spaces. Second, we provide a Java-based automated reasoner that supports these operations for both approaches, thus eliminating the burden of selecting the appropriate tool and approach depending on the operation one wants to perform.

翻译：分析特征模型（FM）并对其对应的配置空间进行推理是软件产品线（SPL）工程中的核心任务。诸如判定FM的可满足性及消除FM中不一致部分等问题，已通过将FM转换为合取范式（CNF）公式、再将CNF输入SAT求解器的方式得到有效解决。然而，该方法在应对其他重要推理问题（如配置计数或枚举）时存在局限性。目前学界主要研究了两种主流方法：（i）直接方法——直接利用基于当前FM的CNF表示的工具；（ii）基于编译的方法——先将FM的CNF表示转换为更易于处理推理查询的其他表示形式。我们的贡献体现在两方面：首先，评估了两种方法在处理FM常见推理操作（包括配置计数、单个或多个配置的列举与采样、以及基于效用函数的最优配置求解）时的性能对比。实验结果表明，基于编译的方法效率足以与直接方法竞争，且在大型配置空间上处理足够多复杂推理操作时，转换成本（即编译时间）可实现平衡。其次，我们提供了一个基于Java的自动化推理器，支持两种方法完成上述操作，从而消除了根据具体任务选择合适工具与方法的负担。