权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

SAT（可满足性）问题的并行局部搜索算法研究及其在大规模并行计算机上的实现

基本信息

批准号：
11F01807
负责人：
稲葉真理
金额：
$ 1.28万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2011
资助国家：
日本
起止时间：
2011 至 2013
项目状态：
已结题

项目摘要

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.

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