基于SAT编码的最大团并行算法的设计、优化及其应用研究

The maximum clique problem, one of the most challenging NP-complete problems in computer science, addresses important questions in bioinformatics and molecular modeling. In this work, we develop novel parallel approaches to solving the maximum clique problem based on SAT. For branch-and-bound Maxclique algorithms, the quality of the upper bound is very important, most of the traditional approaches use the same strategy to compute an upper bound, based on coloring a graph or finding an independent set partition. To avoid the bottleneck of traditional methods, we notice that the Maxclique can be encoded into SAT, and use many SAT technologies to compute an improved upper bound. On the other hand, we design a parallel computational model based on this algorithm for heterogeneous platforms. We investigate data parallelism, memory shared and message passing to exploit the performance potentials of heterogeneous platforms. The results of this project will be directly applied to bio-pharmaceutical, bioinformatics and molecular modeling, and greatly accelerate the development of these industries.

最大团问题是计算机科学领域中一个最具挑战的NP完全问题，它也是生物信息和分子建模等领域中一个非常重要的问题。本项目研究基于SAT编码的并行最大团算法的实现和优化。分支界定算法中的上届计算是非常重要的一个环节，大部分传统做法都使用相同的策略来计算上届，如染色、独立集等。 为了避免传统做法的瓶颈，本项目使用SAT编码刻画最大团问题，然后使用特殊的SAT技术来优化算法上届。另一方面，基于串行算法，设计针对异构体系结构的并行算法，同时优化数据划分，内存共享和消息传递等一系列并行技术，使得算法能够充分利用异构平台的潜能。本项目的研究成果将能直接应用于生物医药等行业，大大加速这些行业的发展。

最大团问题是计算机科学领域中一个最具挑战的NP完全问题，它是经典调度问题、生物信息和分子建模等领域中一个非常重要的问题。本项目研究基于SAT编码的并行最大团算法的实现和优化。通过分支界定严格约束搜索上届，将染色、独立集等作为分支界定的策略成为了很多经典算法的实现手段。为了避免传统做法的瓶颈，我们将把最大团转化成SAT编码，然后使用一些SAT技术来优化算法上届。另一方面，我们基于串行算法，设计了一个针对国产异构体系结构的并行计算，本项目研究了数据划分，内存共享和消息传递等一系列并行技术，使得算法能够充分利用异构平台的潜能。在神威太湖之光上，我们的核心函数并行算法在4主核、256从核的单节点上加速比最大可达到16.4。同时，我们将该并行算法应用于调度、药物预测、分子建模等领域，均取得了不错的效果。