计算机科学 ›› 2024, Vol. 51 ›› Issue (11A): 240300161-5.doi: 10.11896/jsjkx.240300161
郑苏豪1, 牛秦洲1, 陶小梅2
ZHENG Suhao1, NIU Qinzhou1, TAO Xiaomei2
摘要： 伪布尔约束问题是一类与布尔约束问题相似的组合优化难题。解决这类问题的核心在于以不同的数学形式对伪布尔约束进行编码,例如线性规划、整数规划以及其他形式的组合优化。当前流行的解决方法是将问题转化为布尔公式,然后运用冲突导向的子句学习(CDCL)类SAT求解器对这些布尔公式进行求解。提出了一种新的方法来解决伪布尔约束问题中的模型计数问题。首先,介绍了知识编译和扩展规则的相关概念,随后详细阐述了如何利用知识编译将伪布尔约束问题转化为二元决策图(BDD),并着重探讨了BDD结构的特性,最后采用基于扩展规则的模型计数方法来处理伪布尔约束问题中的模型计数问题。实验结果表明,该方法在处理互补因子较高的子句集时表现出更为优越的性能。
中图分类号:
| [1]EÉN N,SÖRENSSON N.Translating pseudo-boolean con-straints into SAT[J].Journal on Satisfiability,Boolean Mode-ling and Computation,2006,2(1/2/3/4):1-26. [2]ABÍO I,NIEUWENHUIS R,OLIVERAS A,et al.A new look at BDDs for pseudo-Boolean constraints[J].Journal of Artificial Intelligence Research,2012,45:443-480. [3]BOFILL M,COLL J,NIGHTINGALE P,et al.SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints[J].Artificial Intelligence,2022,302:103604. [4]DING Z Y.Research and Implementation of Applying LinearAlgebra to Solve Satisfiability Problem[D].Guangzhou:Sun Yat-sen University,2014. [5]FANG C,LIU J.A linear algebra formulation for boolean satis-fiability testing[J].arXiv:1701.02401,2017. [6]HAI L,JIGUI S,YIMIN Z.Theorem proving based on the extension rule[J].Journal of Automated Reasoning,2003,31:11-21. [7]YIN M H,LIN H,SUN J G.Solving #SAT using extensionrules[J].Journal of Software,2009,20(7):1714-1725. [8]JHA A,SUCIU D.Knowledge compilation meets database theory:compiling queries to decision diagrams[C]//Proceedings of the 14th International Conference on Database Theory.2011:162-173. [9]INOUE K.Evaluating abductive hypotheses using an EM algorithm on BDDs[C]//Proc.IJCAI-09.2009:810-815. [10]DARWICHE A.Decomposable negation normal form[J].Journal of the ACM(JACM),2001,48(4):608-647. [11]GU W X.Knowledge Compilation Survey[J].Computer Scien-ce,2010,37(7):7. [12]ZHAO X W.Research of the Knowledge compilation and Contingent Flexible Planning[D].Changchun:Northeast Normal University,2010. [13]LYU S,ZHANG T,WANG Q,et al.Two Novel AlgorithmsBased on Extension Rule for Solving# SAT Problem[J].Journal of Northeastern University(Natural Science),2019,40(5):630. [14]LATOUR A L D,SEN A,MEEL K S.Solving the identifying code set problem with grouped independent support[J].arXiv:2306.15693,2023. [15]AUSIELLO G,CRESCENZI P,GAMBOSI G,et al.Complexity and approximation:Combinatorial optimization problems and their approximability properties[M].Springer Science & Business Media,2012. [16]ROUGHGARDEN T.Algorithmic game theory[J].Communications of the ACM,2010,53(7):78-86. [17]DUDEK J M,PHAN V H N,VARDI M Y.DPMC:weightedmodel counting by dynamic programming on projectjoin trees[C]//International Conference on Principles and Practice of Constraint Programming.Cham:Springer International Publi-shing,2020:211-230. [18]SUZUKI R,HASHIMOTO K,SAKAI M.Improvement of Projected Model-Counting Solver with Component Decomposition Using SAT Solving in Components:JSAI Technical Report:SIG-FPAI[R].2017:31-36. [19]PHILIPP T,STEINKE P.Pblib-a library for encoding pseudo-boolean constraints into cnf[C]//International Conference on Theory and Applications of Satisfiability Testing.Cham:SpringerInternational Publishing,2015:9-16. |
|
||
首页