Research on Model Counting with Mixed Exactly-One Constraints

doi:10.12068/j.issn.1005-3026.2022.04.002

Abstract

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

CLC Number:

TP20

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.

References

[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算法及无偏估计量下界，同时拥有更高的鲁棒性及稳定性，其时间复杂度则基本不高于前人算法.