伪布尔约束的一种模型计数方法  

Model Counting Method for Pseudo-Boolean Constraints

作　　者：郑苏豪 牛秦洲[1] 陶小梅[2] ZHENG Suhao;NIU Qinzhou;TAO Xiaomei(College of Information Science and Engineering,Guilin University of Technology,Guilin,Guangxi 541006,China;School of Computer Science and Engineering&School of Software,Guangxi Normal University,Guilin,Guangxi 541006,China)

机构地区：[1]桂林理工大学信息科学与工程学院,广西桂林541006 [2]广西师范大学计算机科学与工程学院、软件学院,广西桂林541006

出　　处：《计算机科学》2024年第S02期150-154,共5页Computer Science

基　　金：国家自然科学基金(61906051)。

摘　　要：伪布尔约束问题是一类与布尔约束问题相似的组合优化难题。解决这类问题的核心在于以不同的数学形式对伪布尔约束进行编码,例如线性规划、整数规划以及其他形式的组合优化。当前流行的解决方法是将问题转化为布尔公式,然后运用冲突导向的子句学习(CDCL)类SAT求解器对这些布尔公式进行求解。提出了一种新的方法来解决伪布尔约束问题中的模型计数问题。首先,介绍了知识编译和扩展规则的相关概念,随后详细阐述了如何利用知识编译将伪布尔约束问题转化为二元决策图(BDD),并着重探讨了BDD结构的特性,最后采用基于扩展规则的模型计数方法来处理伪布尔约束问题中的模型计数问题。实验结果表明,该方法在处理互补因子较高的子句集时表现出更为优越的性能。Pseudo-Boolean constraints problem is a kind of combinatorial optimization problem similar to the Boolean constraints problem.The core of solving such problems lies in encoding Pseudo-Boolean constraints in different mathematical forms,such as linear programming,integer programming,and other forms of combinatorial optimization.The current popular solution is to convert the problem into Boolean formulas,and then use the conflict-oriented clause learning(CDCL)class SAT solver to solve these Boolean formulas.This paper proposes a new method to solve the model counting problem in the Pseudo-Boolean constraints problem.Firstly,the related concepts of knowledge compilation and extension rules are introduced,and then how to transform Pseudo-Boolean constraints problem into binary decision diagram(BDD)by knowledge compilation is discussed in detail,and the characteristics of BDD structure are discussed emphatically.Finally,the model counting method based on extension rules is adopted to deal with the model counting problem in Pseudo-Boolean constraints problem.Experimental results show that the proposed method has better performance when dealing with clauses with higher complementarity factors.

关 键 词：伪布尔约束 SAT问题 模型计数 知识编译 子句 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]