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

该项目的总体结果可以分为三个主要类别：大规模并行局部搜索的合作;并行SAT局部搜索的性能估计;以及局部搜索求解器的GPU实现。首先，我们发现SAT大规模并行本地搜索求解器中的合作是一项强大的技术，有助于将性能提高到给定数量的核心（通常是16个核心），然后性能就会下降。然而，当合作仅限于一组求解器的并行局部搜索求解器的性能扩展以及高达几百core.Second，我们的模型来预测并行局部搜索求解器密切匹配的经验评估高达384个核心，为最佳的求解器的SAT 2011年的竞争和两组问题的家庭，即随机和精心制作的。我们的模型，顺序统计的基础上，预测并行运行时执行给定的本地搜索算法，通过分析其顺序版本的运行时分布。有趣的是，我们观察到，对于两个不同的顺序求解器和本研究中考虑的各种实例，运行时分布可以使用两种分布来表征：指数第三，与依赖于问题并且联合收割机组合CPU和GPU的执行的其他局部搜索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.