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

Research on Model Counting with Mixed Exactly-One Constraints

作　　者：韩淑婷 赖永[1,2] 刘杰[1,2] HAN Shu-ting;LAI Yong;LIU Jie(College of Computer Science and Technology,Jilin University,Changchun 130012,China;Key Laboratory of Symbolic Computation and Knowledge Engineering,Ministry of Education,Changchun 130012,China)

机构地区：[1]吉林大学计算机科学与技术学院,吉林长春130012 [2]吉林大学符号计算与知识工程教育部重点实验室,吉林长春130012

出　　处：《东北大学学报（自然科学版）》2022年第4期463-469,共7页Journal of Northeastern University(Natural Science)

基　　金：国家自然科学基金资助项目(61976050);吉林省自然科学基金资助项目(20190103005JH).

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

关 键 词：exactly-one约束 模型计数 二元约束传播 合取范式 C2D 

分 类 号：TP20[自动化与计算机技术—检测技术与自动化装置]