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

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

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.