Dynamic Blocked Clause Elimination for Projected Model Counting

要約

このペーパーでは、予測モデルのカウントに対するブロックされた句の削除の適用を検討します。
これはモデルの数を決定する問題です ||\exists X.{\Sigma}||
与えられた変数の集合 X を存在的に消去した後の命題式 {\Sigma} の計算。
ブロックされた文節の削除は SAT を解くためのよく知られた手法ですが、一般にモデルの数が変更されるため、モデルのカウントに直接適用するのは困難です。
ただし、ブロックされた文節の検索中に射影された変数に焦点を当てることで、正しいモデル数を維持しながらブロックされた文節の削除を活用できることを示します。
モデルのカウント中にブロックされた文節の削除を効率的に利用するために、新しいデータ構造と関連アルゴリズムが導入されています。
私たちが提案したアプローチはモデルカウンター d4 に実装されています。
私たちの実験は、予測モデルのカウントに対するブロックされた節の削除という新しい方法の計算上の利点を示しています。

要約(オリジナル)

In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ||\exists X.{\Sigma}|| of a propositional formula {\Sigma} after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google