arXiv:2505.05976cs.AIcs.LO2025-05

提出伪布尔d-DNNF编译方法,让复杂特征模型推理更快更高效。

Pseudo-Boolean d-DNNF Compilation for Expressive Feature Modeling Constructs

  • 用伪布尔编码替代传统布尔编码,压缩表达复杂约束
  • 新编译方法使特征模型转换速度显著提升,尤其在复杂构造下
  • 适合需要高效分析的复杂配置系统设计场景

可配置系统通常由具有依赖关系的可复用组件构成,常用特征模型来描述这些依赖。实际中的特征模型往往复杂,需借助自动化推理分析依赖关系。目前主流做法是将特征模型转化为合取范式(CNF),以便使用现成的SAT或#SAT求解器。然而,现代特征建模语言中的某些构造(如基数约束)难以高效转为CNF,造成表达力与推理效率之间的不匹配。本文提出两方面贡献:首先,提供一种伪布尔编码方式,相比布尔编码能更紧凑地表示常见构造;其次,提出一种将伪布尔公式编译为布尔d-DNNF的新方法。基于编译后的d-DNNF,可直接应用大量已有的高效分析技术。实验表明,本方法在支持表达性构造的特征模型上,显著优于基于CNF的现有方案。所有测试数据集均显示,伪布尔转换速度远快于传统CNF转换。整体而言,采用该方法可大幅加速含复杂约束特征模型的d-DNNF生成。此外,对于仅含基础构造的模型,本方法仍具备竞争力。

原文摘要 · Abstract (English)

Configurable systems typically consist of reusable assets that have dependencies between each other. To specify such dependencies, feature models are commonly used. As feature models in practice are often complex, automated reasoning is typically employed to analyze the dependencies. Here, the de facto standard is translating the feature model to conjunctive normal form (CNF) to enable employing off-the-shelf tools, such as SAT or #SAT solvers. However, modern feature-modeling dialects often contain constructs, such as cardinality constraints, that are ill-suited for conversion to CNF. This mismatch between the input of reasoning engines and the available feature-modeling dialects limits the applicability of the more expressive constructs. In this work, we shorten this gap between expressive constructs and scalable automated reasoning. Our contribution is twofold: First, we provide a pseudo-Boolean encoding for feature models, which facilitates smaller representations of commonly employed constructs compared to Boolean encoding. Second, we propose a novel method to compile pseudo-Boolean formulas to Boolean d-DNNF. With the compiled d-DNNFs, we can resort to a plethora of efficient analyses already used in feature modeling. Our empirical evaluation shows that our proposal substantially outperforms the state-of-the-art based on CNF inputs for expressive constructs. For every considered dataset representing different feature models and feature-modeling constructs, the feature models can be significantly faster translated to pseudo-Boolean than to CNF. Overall, deriving d-DNNFs from a feature model with the targeted expressive constraints can be substantially accelerated using our pseudo-Boolean approach. Furthermore, our approach is competitive on feature models with only basic constructs.

特征建模逻辑编译形式化方法

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。