一句话：系统比较三种 CNF 变换对特征模型分析的正确性与性能影响，揭示 Tseitin 等变换并非总是适用。
特征模型广泛用于建模可变软件系统的特征及其依赖关系，通常需转换为命题公式并交给求解器分析；由于多数求解器仅接受合取范式（CNF），必须进行 CNF 变换。本文比较三种变换：分配律、Tseitin 与 Plaisted-Greenbaum，分析它们能否正确支持各类特征模型分析，并用 FeatureIDE、KConfigReader 与 Z3 三个工具在 22 个真实特征模型语料上评估。结果表明，部分 CNF 变换难以扩展到复杂模型，甚至会在模型计数分析中产生错误结果；此外，CNF 变换的选择会显著影响后续分析性能。
Feature modeling is widely used to systematically model features of variant-rich software systems and their dependencies. By translating feature models into propositional formulas and analyzing them with solvers, a wide range of automated analyses across all phases of the software development process become possible. Most solvers only accept formulas in conjunctive normal form (CNF), so an additional transformation of feature models is often necessary. However, it is unclear whether this transformation has a noticeable impact on analyses. In this paper, we compare three transformations (i.e., distributive, Tseitin, and Plaisted-Greenbaum) for bringing feature-model formulas into CNF. We analyze which transformation can be used to correctly perform feature-model analyses and evaluate three CNF transformation tools (i.e., FeatureIDE, KConfigReader, and Z3) on a corpus of 22 real-world feature models. Our empirical evaluation illustrates that some CNF transformations do not scale to complex feature models or even lead to wrong results for model-counting analyses. Further, the choice of the CNF transformation can substantially influence the performance of subsequent analyses.
@inproceedings{paperbot7207,
title = {Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses},
author = {Elias Kuiter and Sebastian Krieter and Chico Sundermann and Thomas Thüm and Gunter Saake},
booktitle = {ASE},
year = {2022},
doi = {10.1145/3551349.3556938}
}