论文标题
DPMC：通过在项目加入树上动态编程计数的加权模型
DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees
论文作者
论文摘要
我们提出了一个统一的动态编程框架，以计算以结合形式的公式的精确文字加权模型计数。框架的中心是项目加入树，该树指定有效的项目加入订单以应用添加剂预测（可变消除）和加入（子句乘法）。在此框架中，模型计数分为两个阶段。首先，计划阶段从公式中构造了一个项目加入树。其次，执行阶段计算公式的模型计数，采用由项目加入树指导的动态编程。我们从经验上评估了计划阶段的各种方法，并将约束 - 满足启发式方法与树分解工具进行比较。我们还研究了执行阶段的不同数据结构的性能，并将代数决策图与张量进行比较。我们表明，我们的动态编程模型计数框架DPMC与最新的精确加权模型计数器Cachet，C2D，D4和Minic2d具有竞争力。
We propose a unifying dynamic-programming framework to compute exact literal-weighted model counts of formulas in conjunctive normal form. At the center of our framework are project-join trees, which specify efficient project-join orders to apply additive projections (variable eliminations) and joins (clause multiplications). In this framework, model counting is performed in two phases. First, the planning phase constructs a project-join tree from a formula. Second, the execution phase computes the model count of the formula, employing dynamic programming as guided by the project-join tree. We empirically evaluate various methods for the planning phase and compare constraint-satisfaction heuristics with tree-decomposition tools. We also investigate the performance of different data structures for the execution phase and compare algebraic decision diagrams with tensors. We show that our dynamic-programming model-counting framework DPMC is competitive with the state-of-the-art exact weighted model counters cachet, c2d, d4, and miniC2D.
