Engineering an Exact Pseudo-Boolean Model Counter

要約

コンピューター サイエンスの基本的なタスクであるモデルのカウントには、通常結合正規形 (CNF) で表されるブール式への満足のいく代入の数を決定することが含まれます。
CNF 公式のモデル カウンティングは幅広い用途で注目を集めていますが、擬似ブール (PB) 公式のモデル カウンティングの研究は比較的無視されてきました。
擬似ブール式は命題ブール式よりも簡潔であるため、現実世界の問題をより柔軟に表現できます。
したがって、PB 式のモデル計数のための効率的な手法を調査することが極めて重要です。
この研究では、代数決定図による知識編集アプローチに依存する、最初の正確な擬似ブール モデル カウンター PBCount を提案します。
私たちの広範な経験的評価により、現在の最先端のアプローチでは 1013 個のインスタンスしか処理できないのに対し、PBCount は 1513 個のインスタンスのカウントを計算できることが示されています。
私たちの研究は、前処理技術の開発や知識の編集以外のアプローチの探求など、PB 式のモデル計数に関連した将来の研究にいくつかの道を開きます。

要約(オリジナル)

Model counting, a fundamental task in computer science, involves determining the number of satisfying assignments to a Boolean formula, typically represented in conjunctive normal form (CNF). While model counting for CNF formulas has received extensive attention with a broad range of applications, the study of model counting for Pseudo-Boolean (PB) formulas has been relatively overlooked. Pseudo-Boolean formulas, being more succinct than propositional Boolean formulas, offer greater flexibility in representing real-world problems. Consequently, there is a crucial need to investigate efficient techniques for model counting for PB formulas. In this work, we propose the first exact Pseudo-Boolean model counter, PBCount, that relies on knowledge compilation approach via algebraic decision diagrams. Our extensive empirical evaluation shows that PBCount can compute counts for 1513 instances while the current state-of-the-art approach could only handle 1013 instances. Our work opens up several avenues for future work in the context of model counting for PB formulas, such as the development of preprocessing techniques and exploration of approaches other than knowledge compilation.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google