ADDMC:基于代数决策图的加权模型计数
计算机科学中的逻辑
2020-06-03 v2 人工智能
数据结构与算法
摘要
我们提出一种算法,用于计算合取范式下布尔公式的精确文字加权模型计数。我们的算法采用动态规划,并使用代数决策图作为主要数据结构。我们在新的模型计数器 ADDMC 中实现了该技术。我们实证评估了可与 ADDMC 一起使用的各种启发式方法。然后我们在 1914 个标准模型计数基准上将 ADDMC 与最先进的精确加权模型计数器(Cachet、c2d、d4 和 miniC2D)进行比较,并表明 ADDMC 显著改进了虚拟最佳求解器。
引用
@article{arxiv.1907.05000,
title = {ADDMC: Weighted Model Counting with Algebraic Decision Diagrams},
author = {Jeffrey M. Dudek and Vu H. N. Phan and Moshe Y. Vardi},
journal= {arXiv preprint arXiv:1907.05000},
year = {2020}
}
备注
Presented at AAAI 2020