【摘要】 伪布尔约束问题是一类与布尔约束问题相似的组合优化难题。解决这类问题的核心在于以不同的数学形式对伪布尔约束进行编码，例如线性规划、整数规划以及其他形式的组合优化。当前流行的解决方法是将问题转化为布尔公式，然后运用冲突导向的子句学习（CDCL）类SAT求解器对这些布尔公式进行求解。提出了一种新的方法来解决伪布尔约束问题中的模型计数问题。首先，介绍了知识编译和扩展规则的相关概念，随后详细阐述了如何利用知识编译将伪布尔约束问题转化为二元决策图（BDD），并着重探讨了BDD结构的特性，最后采用基于扩展规则的模型计数方法来处理伪布尔约束问题中的模型计数问题。实验结果表明，该方法在处理互补因子较高的子句集时表现出更为优越的性能。更多还原

【Abstract】 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.更多还原