混合exactly-one约束的模型计数研究

模型计数是求给定命题公式的模型数，是人工智能领域的一个基本问题.在贝叶斯网络、有界模型检测、精确集合覆盖等众多实际问题中，存在许多exactly-one约束.常见的处理方法是将exactly-one约束编码为CNF公式，再调用模型计数器求解.这种方法扩大了命题公式的规模，容易导致求解时间过长.本文分别提出从CNF公式中还原exactly-one约束的ECR算法和处理exactly-one约束的ECP算法.ECR算法能明显提高C2D编译器的求解效率.基于最新的模型计数器ExactMC，本文改进了能识别和单独处理exactly-one约束的模型计数器ECMC.实验结果表明，ECMC的时间效率相比ExactMC有显著提高.

Research on Model Counting with Mixed Exactly-One Constraints

Model counting is the number of models for a given proposition formula， which is a basic problem in the field of artificial intelligence. There are many exactly-one constraints in many practical problems such as Bayesian networks， bounded model detection， and accurate set coverage. A common processing method is to encode exactly-one constraints as CNF formulas， and then call the model counter to solve them. This method expands the scale of the proposition formula and easily leads to too long solution time. This paper respectively proposes the ECR algorithm that restores exactly-one constraints from the CNF formula and the ECP algorithm that handles exactly-one constraints. The ECR algorithm can significantly improve the solution efficiency of the C2D compiler. Based on the latest model counter ExactMC， this paper improves the model counter ECMC that can recognize and handle exactly-one constraints separately. The experimental results show that the time efficiency of ECMC is significantly improved compared to ExactMC.