模型计数问题精确求解方法的研究

Model counting is a problem of computing the number of models for a given propositional formula. Recently, model counting has been successfully applied to probabilistic inference problems, combinatorial problems, intelligent planning problems, and aerospace field, etc. However, the state-of-the-art exact model counters can only tackle problem with a couple of hundred variables. In addition, the efficiencies of the current exact model counters are less than the best SAT solvers. Thus, it becomes an urgent problem that how to address exact model counting algorithms which can efficiently tackle large formulae. The project will be focus on the methods for solving exact model counting problem. First of all, we shall present effective reduction strategies. Secondly, we shall study the relationship between the different sizes of backbone variable set and the solution space. In addition, we shall address the algorithms for determining the backbone variables. Thirdly, we shall study knowledge compilation approaches, present tractable compilation languages, provide the effective compilation approaches. Fourthly, we shall design efficient algorithms for solving exact model counting problem, and develop the exact counters that can solving large formulae. Finally, we aim at establishing the model counting solving theories and methods with our own characteristic in the international area.

模型计数问题是指计算给定命题公式的模型的个数。近年来，模型计数问题已经成功应用于概率推理、组合优化、智能规划、航空航天等领域。但迄今为止，模型计数问题精确求解器只能求解几百个变量规模的模型计数问题实例，求解效率与SAT问题求解器还存在很大差距，如何设计出高效地求解大规模模型计数问题实例的精确算法便成为了一个亟需解决的问题。因此，本项目将围绕模型计数问题精确求解方法这一核心内容展开，提出高效的简化策略；研究不同大小的骨架变量集合与解空间的关系，提出骨架变量的求解算法；研究知识编译方法各自适应的问题类型，提出新的支持易处理的模型计数操作的编译语言，并给出有效的编译方法；有针对性地设计高效的模型计数问题精确求解算法，开发能够快速求解大规模模型计数问题实例的求解器，最终建立国际上有我们自己特色的、成体系的模型计数问题求解理论和方法。

近年来，模型计数问题已经成功应用于概率推理、组合优化、智能规划、航空航天等领域。本课题组针对模型计数问题做了较为深入、细致的研究，并取得了较为满意的成果，主要包括：. 1）问题的结构方面，通过研究可以在多项式时间内转换为模型计数问题公式形式的CSP问题的社区结构，利用模块化的值检测具有RB模型CSP问题中是否存在社区结构，并且讨论社区结构与RB模型参数之间的关系，进一步帮助了我们理解模型计数问题的结构特征。. 2）问题的复杂性方面，研究了模型计数的基础问题NAE k-SAT(b)问题的相变，从理论上证明了这类问题存在着从可满足到不可满足的突变，在求解过程中存在easy-hard-easy模型。另外，还研究了Max NAE SAT问题的相变规律，理论上给出了求解Max NAE SAT问题的上界。. 3）问题的求解方面，本项目设计并实现了计数可满足性模理论问题求解器，基于加强式格局检测策略的最小可满足性问题求解器，加权顶点覆盖问题求解器，最小连通支配集问题求解器等。实验表明，这些求解器在求解规模和效率上有显著的提高。. 上述研究挖掘和发现了问题的求解规律，使得研究人员能够更好的理解问题的本质，有针对性的设计高效算法，成功地提高了问题的求解效率，进一步推动了模型计数问题求解的研究。