ADDMC：使用代数决策图的精确加权模型计数

作者：Jeffrey M. Dudek,Vu H. N. Phan,Moshe Y. Vardi

摘要：ADDMC：使用代数决策图的精确加权模型计数

我们计算CNF公式的精确文字加权模型计数。 我们的算法采用动态规划，代数决策图作为主要数据结构。 这种技术在ADDMC中实现，ADDMC是一种新的模型计数器。 我们根据经验评估可与ADDMC一起使用的各种启发式方法。 我们还在两个最大的CNF模型计数基准系列（BayesNet和Planning）上将ADDMC与最先进的精确模型计数器（Cachet，c2d，d4，miniC2D和sharpSAT）进行了比较。 ADDMC在给定的超时内解决了总计最多的基准。...

原文标题：ADDMC: Exact Weighted Model Counting with Algebraic Decision Diagrams

原文摘要：We compute exact literal-weighted model counts of CNF formulas. Our algorithm employs dynamic programming, with Algebraic Decision Diagrams as the primary data structure. This technique is implemented in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We also compare ADDMC to state-of-the-art exact model counters (Cachet, c2d, d4, miniC2D, and sharpSAT) on the two largest CNF model counting benchmark families (BayesNet and Planning). ADDMC solves the most benchmarks in total within the given timeout.

地址：https://arxiv.org/abs/1907.05000