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

要約

構成可能なシステムは通常、互いに依存関係を持つ再利用可能な資産で構成されています。
このような依存関係を指定するために、特徴モデルが一般的に使用されます。
実際の機能モデルは複雑であるため、通常、自動化された推論が依存関係を分析するために採用されています。
ここでは、事実上の標準は、SATや#SATソルバーなどの既製のツールを採用できるように、機能モデルを組み合わせの通常のフォーム（CNF）に翻訳しています。
ただし、最新の機能モデリング方言には、CNFへの変換に適していないカーディナリティの制約などの構造物が含まれています。
推論エンジンの入力と利用可能な機能モデリングの方言との間のこの不一致は、より表現力のある構造の適用性を制限します。
この作業では、表現力豊かな構造とスケーラブルな自動化された推論との間のこのギャップを短縮します。
私たちの貢献は2つあります。まず、特徴モデル向けの擬似ブールのエンコードを提供します。これにより、ブールエンコードと比較して、一般的に使用されるコンストラクトの小さな表現が容易になります。
第二に、擬似ブール式をブールd-dnnfにコンパイルする新しい方法を提案します。
コンパイルされたD-DNNFSを使用すると、機能モデリングですでに使用されている多くの効率的な分析に頼ることができます。
私たちの経験的評価は、私たちの提案が表現力豊かな構造のCNF入力に基づいて、最先端を大幅に上回ることを示しています。
さまざまな機能モデルと機能モデリングコンストラクトを表すすべてのデータセットについて、機能モデルはCNFよりも擬似ブールに翻訳されることが大幅に高速になります。
全体として、ターゲットを絞った表現的制約を備えた機能モデルからD-DNNFを導き出すことは、擬似ブールのアプローチを使用して実質的に加速できます。
さらに、私たちのアプローチは、基本的なコンストラクトのみを備えた機能モデルで競争力があります。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google