计数约束满足问题的相变现象研究

In the decade, we have viewed increasing interest in the problem of counting constraint satisfaction problem (#CSP for short), due to its great success in the application field such as automated planning and software engineering.Professor Valiant, who won 2010 Turing Award, has predicted that #P-hard problems including #CSP will be one of the most important research direction in the future.Although the research of phase transition in constraint satisfaction problem (CSP for short) has achieved a lot of success, few researchers have focused on phase transition of #CSP until now. Based on previous work made by our group, in this project, we shall study the phenomenon of counting satisfaction problems of different random model. First of all, we shall prove the existence of phase transitions and obtain the location of phase transition thresholds. After that, we shall generate hard random instances as the benchmark of counting constraint satisfaction problem algorithms. Then, we shall study the structure of the problems to provide theoretical evidence of the intractability of the random instances around the phase transition thresholds. Accordingly, we shall develop efficient algorithms to solve those hard instances.

近年来随着计数约束满足问题在智能规划、航空航天、软件工程等应用领域的广泛应用，研究人员对其的关注提高到前所未有的高度。2010年图灵奖获得者哈佛大学的Valiant教授曾多次指出计数约束满足等#P难问题将成为计算机科学领域未来最重要的研究论题之一。尽管对约束满足问题的相变现象的研究已经取得了令人瞩目的成功，但是对计数约束满足问题的相变现象的研究尚属起步阶段。本项目将围绕计数约束满足问题的相变现象这一核心内容开展研究：研究不同随机模型的计数约束满足问题的相变规律，确定计数约束满足问题相变点位置；在此基础上，生成计数约束满足问题的难解实例作为算法测试集；研究技术约束满足问题的结构特征与相变现象之间的关系，为难解性提供理论证据；有针对性的设计高效的计数约束满足问题的求解算法。

计数约束满足问题是是最早被证明为#P完全 (#P-complete)的问题，也是#P复杂类中的核心问题之一，在智能规划、概率推理、航空航天、软件工程等领域有着广泛的应用。对计数约束满足问题相变现象的研究不仅有助于揭示问题难解的本质，而且有助于设计高效的问题求解算法。本项目围绕计数约束满足问题的相变现象这一核心内容展开，包括如下几方面内容：.1）在相变点确定方面，研究了计数约束满足问题、约束优化问题、NAE k-SAT(b)问题等难解问题的相变规律，从理论和实验角度验证了这些问题均存在easy-hard-easy模式和相变现象，同时研究和分析了问题相变点所在区域的上界和下界。.2）在问题结构特征与相变现象关系方面，项目组在OBDD语言的基础上提出了多个知识编译目标语言，分析了知识编译目标语言和计数约束满足问题相变现象之间的关系。此外，项目组还研究了约束图中的超树宽度、环割集、联通支配集等结构特征与相变现象和问题求解之间的难度关系，为计数约束满足问题的难解性提供了理论证据。.3）通过研究算法在相变区失效的原因，项目组设计了求解较大规模#SMT 实例的求解算法、求解#XSAT问题的高效问题求解算法、以及求解模型计数问题的近似求解算法，此外，项目组通过研究支配集、最大加权团等问题的相变现象，设计了多个高效的问题求解器。. 总体来说，本项研究确定了问题相变区和难解区的上下界，是计数约束满足问题研究领域难解性刻画中的重要一环。另一方面，对相变现象的研究，还有助于我们设计高效的问题求解算法。