利用 d-DNNF 进行特征模型上的重复计数查询
软件工程
2023-03-23 v1 计算机科学中的逻辑
摘要
特征模型通常用于指定产品线的有效配置。在工业界，由于特征与约束数量庞大，特征模型往往十分复杂。因此，已提出大量自动化分析方法。其中许多依赖于计算有效配置的数量，这通常需解决 #SAT 问题，一项计算代价高昂的操作。此外，大多数基于计数的分析需要在同一特征模型上多次进行 #SAT 计算。特别是，许多分析依赖于多次计算以评估包含特定特征或符合部分配置的有效配置数量。我们旨在通过在高度相似公式的多次计算间复用知识来提升性能，而非使用昂贵的重复计算。本工作中，我们首次提出复用 d-DNNF 以在特征与部分配置上执行高效的重复查询。我们的实证评估表明，相较于重复调用 #SAT 求解器的最先进方法，我们的方法最高快 8,300 倍（节省 99.99% CPU 时间）。与使用 #SAT 求解器相比，应用我们的工具 ddnnife 将运行时间从数天缩短至数分钟。
引用
@article{arxiv.2303.12383,
title = {Exploiting d-DNNFs for Repetitive Counting Queries on Feature Models},
author = {Chico Sundermann and Heiko Raab and Tobias Heß and Thomas Thüm and Ina Schaefer},
journal= {arXiv preprint arXiv:2303.12383},
year = {2023}
}