arXiv:2505.05976v1 宣告类型: 新 摘要: 可配置系统通常由相互依赖的可重用组件组成。为了指定这些依赖关系，通常使用功能模型。由于在实践中功能模型往往非常复杂，因此通常采用自动化推理方法来分析这些依赖关系。目前，将功能模型转换为合取范式（CNF）已成为一种事实上的标准做法，这使得可以利用现成的工具，例如SAT或#SAT求解器。然而，现代功能建模方言中常包含不适合转换为CNF的构造，如基数约束。这种推理引擎的输入与可用的功能建模方言之间的不匹配限制了更具表现力的构造的应用。在本文中，我们缩短了表达能力强的构造与可扩展自动化推理之间的差距。我们的贡献主要有两点：首先，我们提供了一种伪布尔编码方法，相对于布尔编码，该方法可以更简洁地表示常用的构造。其次，我们提出了一种将伪布尔公式编译为布尔d-DNNF的新方法。通过编译的d-DNNF，我们可以利用功能建模中已经广泛使用的高效分析方法。我们的实证评估表明，在针对表达性强的功能模型的输入时，我们的建议相对于使用CNF输入的方法显著提高了表现。对于代表不同类型功能模型和功能建模构造的每一个已考虑的数据集，相比于转换为CNF，功能模型可以显著更快地转换为伪布尔公式。总体而言，使用我们的伪布尔方法可以从具有目标表现力约束的功能模型中更加快速地推导出d-DNNF。此外，对于仅包含基本构造的功能模型，我们的方法也具有竞争力。