DPMC：基于投影-连接树动态规划的加权模型计数
计算机科学中的逻辑
2020-08-21 v1 人工智能
数据结构与算法
摘要
我们提出了一个统一的动态规划框架，用于计算合取范式公式的精确字面量加权模型计数。我们框架的核心在于投影-连接树，其指定了高效的投影-连接顺序，以应用加性投影（变量消去）与连接（子句相乘）。在该框架中，模型计数分两个阶段执行。首先，规划阶段从公式构造投影-连接树。其次，执行阶段依据投影-连接树的引导，采用动态规划计算公式的模型计数。我们实证评估了规划阶段的多种方法，并将约束满足启发式与树分解工具进行比较。我们还研究了执行阶段不同数据结构的性能，并比较了代数决策图与张量。我们表明，我们的动态规划模型计数框架 DPMC 与最先进的精确加权模型计数器 cachet、c2d、d4 和 miniC2D 相比具有竞争力。
引用
@article{arxiv.2008.08748,
title = {DPMC: Weighted Model Counting by Dynamic Programming on Project-Join Trees},
author = {Jeffrey M. Dudek and Vu H. N. Phan and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:2008.08748},
year = {2020}
}
备注
Full version of paper at CP 2020 (26th International Conference on Principles and Practice of Constraint Programming)