SAT(充足可能性)問題の並列局所探索アルゴリズムの研究と超並列計算機への実装

该项目的总体结果可分为三大类：大规模并行本地搜索的合作；估计并行SAT局部搜索的性能；以及本地搜索求解器的GPU实现。首先，我们发现大规模并行局部搜索求解器的协作是一种强大的技术，有助于提高性能到给定的核心数量（通常是16个核心），超过这个点性能就会下降。然而，当合作仅限于一组求解器时，并行局部搜索求解器的性能可以扩展到几百个核。其次，我们预测并行局部搜索解的模型与384个核心的实证评估非常吻合，针对2011年SAT竞赛的最佳解和两组问题族，即随机和精心设计。我们的模型基于顺序统计，通过分析顺序版本的运行时分布来预测给定局部搜索算法的并行运行时执行情况。有趣的是，我们已经观察到，对于本研究中考虑的两个不同的顺序求解器和各种实例，运行时分布可以使用两个分布来表征：指数分布（移位和非移位）和对数正态分布。第三，与其他局部搜索GPU实现不同，这些实现依赖于问题并结合CPU和GPU的执行，在这项工作中，整个局部搜索过程都在GPU上执行；因此，性能并不局限于一个健壮的CPU。使用三个众所周知的问题基准进行的大量实验表明，GPU w.r. t.是算法的一个经过良好调优的顺序版本。和GPU。

The overall results of the project can be divided into three main categories : cooperation in massively parallel local search ; estimating the performance of parallel SAT local search ; and a GPU implementation of local search solvers. First, we found out that cooperation in massively parallel local search solver for SAT is a powerful technique that helps to improve performance up to a given number of cores (usually 16 cores), and after this point the performance degrades. However, when cooperation is limited to a group of solvers the performance of the parallel local search solver scales well up to a few hundred cores.Second, our model to predict the parallel local search solvers closely matches the empirical evaluation up 384 cores, for the best solvers of the SAT 2011 competition and two set of problem families, that is, random and crafted. Our model, based in order statistics, predicts the parallel runtime execution of a given local search algorithm by analyzing the runtime distribution of its sequential version. Interestingly, we have observed that, for the two different sequential solvers and the variety of instances considered in this study, the runtime distribution can be characterized using two distributions : exponential (shifted and non-shifted) and lognormal.Third, unlike other local search GPU implementations, which are problem dependent and combine the execution of the CPU and the GPU, in this work the entire local search process is executed on the GPU ; therefore, the performance is not bounded to a robust CPU. Extensive experiments using three well-known problem benchmarks indicate that the GPU w. r. t. a well tuned sequential version of the algorithm. and the GPU.