利用伪布尔d-DNNF编译技术处理表达性特征建模结构

《IEEE Transactions on Software Engineering》：Tackling Expressive Feature-Modeling Constructs with Pseudo-Boolean d-DNNF Compilation

　　

摘要：

可配置系统通常由相互依赖的可重用组件构成。为了指定这些依赖关系，通常会使用特征模型。由于实际中的特征模型往往较为复杂，因此通常会采用自动化推理来分析这些依赖关系。目前的事实标准是将特征模型转换为合取范式（CNF），以便使用现成的工具（如SAT或#SAT求解器）进行处理。然而，现代的特征建模语言中包含了一些不适合转换为CNF的结构，例如基数约束。这种推理引擎的输入与可用特征建模语言之间的不匹配限制了这些更具表现力的结构的适用性。在这项工作中，我们缩小了这种表现力结构与可扩展自动化推理之间的差距。我们的贡献有两个方面：首先，我们为特征模型提供了一种伪布尔编码方法，与布尔编码相比，这种方法可以更简洁地表示常用的结构；其次，我们提出了一种将伪布尔公式编译为布尔d-DNNF的新方法。利用编译后的d-DNNF，我们可以应用许多已经在特征建模中使用的高效分析方法。我们的实证评估表明，与基于CNF输入的方法相比，我们的方法在处理具有表现力结构的场景时性能显著提升。对于每个代表不同特征模型和特征建模结构的数据集，将特征模型转换为伪布尔形式的速度明显快于转换为CNF的形式。总体而言，使用我们的伪布尔方法可以从具有特定表现力约束的特征模型中更快地生成d-DNNF。例如，布尔方法仅适用于最多包含13个特征的情况，而伪布尔d-DNNF编译方法可以处理包含数千个特征的情况。此外，我们的方法在处理只有基本约束的特征模型时也具有竞争力...

显示更多