Towards Projected and Incremental Pseudo-Boolean Model Counting

要約

モデルのカウントは、通常論理積正規形 (CNF) で行われる論理式への満足のいく代入の数を決定することを含む基本的なタスクです。
CNF モデル カウンティングはここ数十年にわたって広く注目を集めてきましたが、疑似ブール (PB) モデル カウンティングへの関心は、PB 式の柔軟性の向上も一部の理由として浮上してきたばかりです。
そのため、予測設定や増分設定がサポートされていないなど、既存の PB カウンターには機能のギャップがあり、導入を妨げる可能性があることがわかりました。
この作業における私たちの主な貢献は、PB モデル カウンター PBCount2 の導入です。これは、予測および増分モデル カウントをサポートする最初の正確な PB モデル カウンターです。
私たちのカウンターである PBCount2 は、最小出現加重最小度 (LOW-MD) 計算順序ヒューリスティックを使用して、予測モデルのカウントと増分モデルのカウントを可能にするキャッシュ メカニズムをサポートします。
当社の評価では、PBCount2 は、予測モデル カウンティングでは競合メソッドのベンチマーク数の少なくとも 1.40 倍、インクリメンタル モデル カウンティングでは競合メソッドの少なくとも 1.18 倍のベンチマーク数を完了しました。

要約(オリジナル)

Model counting is a fundamental task that involves determining the number of satisfying assignments to a logical formula, typically in conjunctive normal form (CNF). While CNF model counting has received extensive attention over recent decades, interest in Pseudo-Boolean (PB) model counting is just emerging partly due to the greater flexibility of PB formulas. As such, we observed feature gaps in existing PB counters such as a lack of support for projected and incremental settings, which could hinder adoption. In this work, our main contribution is the introduction of the PB model counter PBCount2, the first exact PB model counter with support for projected and incremental model counting. Our counter, PBCount2, uses our Least Occurrence Weighted Min Degree (LOW-MD) computation ordering heuristic to support projected model counting and a cache mechanism to enable incremental model counting. In our evaluations, PBCount2 completed at least 1.40x the number of benchmarks of competing methods for projected model counting and at least 1.18x of competing methods in incremental model counting.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google