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

doi:10.12068/j.issn.1005-3026.2022.04.002

东北大学学报（自然科学版） ›› 2022, Vol. 43 ›› Issue (4): 463-469.DOI: 10.12068/j.issn.1005-3026.2022.04.002

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

韩淑婷^1,2，赖永^1,2，刘杰^1,2

(1. 吉林大学计算机科学与技术学院，吉林长春130012; 2. 吉林大学符号计算与知识工程教育部重点实验室，吉林长春130012)

修回日期:2021-06-17 接受日期:2021-06-17 发布日期:2022-05-18
通讯作者: 韩淑婷
作者简介:韩淑婷(1998-)，女，河南博爱人，吉林大学硕士研究生; 赖永(1985-)，男，江西萍乡人，吉林大学副教授.
基金资助:
国家自然科学基金资助项目(61976050); 吉林省自然科学基金资助项目(20190103005JH).

Research on Model Counting with Mixed Exactly-One Constraints

HAN Shu-ting^1,2， LAI Yong^1,2， LIU Jie^1,2

1. College of Computer Science and Technology， Jilin University， Changchun 130012， China; 2. Key Laboratory of Symbolic Computation and Knowledge Engineering， Ministry of Education， Changchun 130012， China.

Revised:2021-06-17 Accepted:2021-06-17 Published:2022-05-18
Contact: LIU Jie
About author:-
Supported by:
-

摘要/Abstract

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

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

Abstract: 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.

Key words: exactly-one constraint; model counting; binary constraint propagation; conjunctive normal form; C2D

中图分类号:

TP20

韩淑婷，赖永，刘杰. 混合exactly-one约束的模型计数研究[J]. 东北大学学报（自然科学版）, 2022, 43(4): 463-469.

HAN Shu-ting， LAI Yong， LIU Jie. Research on Model Counting with Mixed Exactly-One Constraints[J]. Journal of Northeastern University(Natural Science), 2022, 43(4): 463-469.

参考文献

[1]Cook S.The complexity of theorem-proving procedures［C］// Proceedings of the Third Annual ACM Symposium on Theory of Computing.Nork York:Association for Computing Machinery，1971:151-158.
[2]贺甫霖，刘磊，吕帅，等.基于格局检测的模型计数方法［J］.软件学报，2020，31(2):395-405.(He Fu-lin，Liu Lei，Lyu Shuai，et al.Model counting methods based on configuration checking［J］.Journal of Software，2020，31(2):395-405.)
[3]Valiant L G.The complexity of enumeration and reliability problems［J］.SIAM Journal on Computing，1979，8(3):410-421.
[4]Bacchus F，Dalmao S，Pitassi T.Algorithms and complexity results for #SAT and Bayesian inference［C］// Proceedings of the 44th Annual IEEE Symposium on Foundations of Computer Science.Cambridge:IEEE Press，2003:340-351.
[5]Roth D.On the hardness of approximate reasoning［J］.Artificial Intelligence，1996，82(1/2):273-302.
[6]Domshlak C，Hoffmann J.Probabilistic planning via heuristic forward search and weighted model counting ［J］.Journal of Artificial Intelligence Research，2011，30(1):565-620.
[7]Biondi F，Enescu M A，Heuser A，et al.Scalable approximation of quantitative information flow in programs［M］.Los Angeles:Springer-Verlag，2018:71-93.
[8]Baluta T，Shen S，Shinde S，et al.Quantitative verification of neural networks and its security applications［C］//Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security.New York:Association for Computing Machinery，2019:1249-1264.
[9]Sang T，Beame P，Kautz H.Heuristics for fast exact model counting［C］// International Conference on Theory & Applications of Satisfiability Testing.Berlin:Springer-Verlag，2005:226-240.
[10]Thurley M.SharpSAT:counting models with advanced component caching and implicit BC［C］// International Conference on Theory and Applications of Satisfiability Testing.Berlin:Springer-Verlag，2006:424-429.
[11]Sharma S，Roy S，Soos M，et al.GANAK:a scalable probabilistic exact model counter［C］//Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence.Macao:IJCAI Press，2019:1169-1176.
[12]Darwiche A.New advances in compiling CNF into decomposable negation normal form［C］// Proceedings of the 16th European Conference on Artificial Intelligence.Amsterdam:IOS Press，2004:328-332.
[13]Darwiche A.Decomposable negation normal form［J］. Journal of the Association for Computing Machinery，2001，48(4):608-647.
[14]吕帅，张桐搏，王强，等.两种新的基于扩展规则#SAT问题求解算法［J］.东北大学学报(自然科学版)，2019，40(5):630-634，646.(Lyu Shuai，Zhang Tong-bo，Wang Qiang，et al.Two novel algorithms based on extension rule for solving #SAT problem［J］.Journal of Northeastern University(Natural Science)，2019，40(5):630-634，646.)
[15]Lai Y，Meel K S，Yap R H C.The power of literal equivalence in model counting［C］// Proceedings of the Thirty-Fifth AAAI Conference on Artificial Intelligence.California:AAAI Press，2021:3851-3859.
[16]Junttila T A，Kaski P.Exact cover via satisfiability:an empirical study［C］// Principles and Practice of Constraint Programming-CP 2010.Berlin:Springer-Verlag，2010:297-304.(上接第462页)Toeplitz矩阵，并将其作为新的自相关矩阵做特征值分解运算得到噪声子空间;对噪声子空间作翻转拆分处理，重构新的求根多项式;最终通过求根运算得到DOA估计值.仿真实验结果表明，相较于部分前人算法，本文算法拥有更高的DOA估计精度，其均方根误差更接近于经典Root-MUSIC算法及无偏估计量下界，同时拥有更高的鲁棒性及稳定性，其时间复杂度则基本不高于前人算法.

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

Research on Model Counting with Mixed Exactly-One Constraints

RichHTML

PDF (PC)

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价

[1]	耿蓉，吴亚倩，肖倩倩，徐赛. 基于改进GRU算法的天基信息网资源预测研究[J]. 东北大学学报（自然科学版）, 2023, 44(3): 305-314.
[2]	罗忠，吴东泽，李雷，葛长闯. 转子系统动力学仿真平台设计与实验验证[J]. 东北大学学报（自然科学版）, 2023, 44(3): 375-381.
[3]	侯振隆，郑玉君，巩恩普，程浩. 基于深度加权的重力梯度数据联合相关成像反演[J]. 东北大学学报:自然科学版, 2020, 41(11): 1628-1632.
[4]	吴超，李元辉，徐帅，戴星航. 地下工程岩体节理迹长统计下限值的确定方法[J]. 东北大学学报:自然科学版, 2020, 41(8): 1167-1173.
[5]	温守钦，唐铁乔，谢伟，付建飞. 氧、硫逸度对岫岩红旗铅锌矿床矿物组合共生分异的制约[J]. 东北大学学报:自然科学版, 2020, 41(7): 999-1007.
[6]	齐锡晶，唐梁，康伟鑫，秦娇娇. 高速公路桥梁桥面板养护方案多目标决策方法[J]. 东北大学学报:自然科学版, 2020, 41(7): 1033-1040.
[7]	蔡志辉，张德良，周彦君，文光奇. 应变速率对Fe-11Mn-2Al-0.2C中锰钢变形行为的影响[J]. 东北大学学报:自然科学版, 2020, 41(7): 1041-1047.
[8]	马树军，王霄霄. 吸附微粒对微悬空桥传感器的影响[J]. 东北大学学报:自然科学版, 2020, 41(1): 108-112.
[9]	马树军，玄航，孙嘉蔚，杨磊. 在非黏性流体域中微悬臂梁振动的建模与仿真[J]. 东北大学学报:自然科学版, 2018, 39(9): 1272-1276.
[10]	马树军，修强. 考虑表面应力的微悬臂梁质量传感器的建模与仿真[J]. 东北大学学报:自然科学版, 2018, 39(2): 237-241.
[11]	陈大力，沈岩涛，谢槟竹，马颖异. 基于余弦相似度模型的最佳教练遴选算法[J]. 东北大学学报:自然科学版, 2014, 35(12): 1697-1700.
[12]	潘峰，刘禄，薛定宇. 最优分数阶PIλDμ网络时延控制器[J]. 东北大学学报:自然科学版, 2014, 35(10): 1382-1385.
[13]	刘禄，潘峰，薛定宇. 一种分数阶卡尔曼滤波器[J]. 东北大学学报:自然科学版, 2014, 35(8): 1069-1072.
[14]	刘金海，冯健，马大中. 流体管道压力信号的高精度实时滤波方法[J]. 东北大学学报:自然科学版, 2013, 34(1): 9-12.
[15]	孙艳蕊. 带时间和成本约束的随机流网络可靠度的计算[J]. 东北大学学报（自然科学版）, 2013, 34(11): 1537-1541.