Using sequential runtime distributions for the parallel speedup prediction of SAT local search
Using sequential runtime distributions for the parallel speedup prediction of SAT local search
复制标题
DOI：
10.1017/s1471068413000392
复制
发表时间：
2013-07-01
影响因子：
1.4
通讯作者：
Codognet, Philippe
中科院分区：
文献类型：
--
作者：
Arbelaez, Alejandro;Truchet, Charlotte;Codognet, Philippe
本文详细分析了可满足性问题局部搜索算法的可扩展性和并行化问题。我们提出了一个框架来估计一个给定的算法的并行性能，通过分析其顺序版本的运行时行为。实际上，通过用统计方法近似顺序进程的运行时分布，并行进程的运行时行为可以通过基于顺序统计的模型来预测。我们应用这种方法来研究两个SAT本地搜索求解器，即麻雀和CCASAT的并行性能，并比较预测的性能的并行硬件上的实际实验结果高达384个核心。我们表明，该模型是准确的，预测性能接近的经验数据。此外，当我们研究不同类型的实例（随机和手工）时，我们观察到本地搜索求解器表现出不同的行为，并且它们的运行时分布可以近似为两种类型的分布：指数分布（移位和非移位）和对数正态分布。
This paper presents a detailed analysis of the scalability and parallelization of local search algorithms for the Satisfiability problem. We propose a framework to estimate the parallel performance of a given algorithm by analyzing the runtime behavior of its sequential version. Indeed, by approximating the runtime distribution of the sequential process with statistical methods, the runtime behavior of the parallel process can be predicted by a model based on order statistics. We apply this approach to study the parallel performance of two SAT local search solvers, namely Sparrow and CCASAT, and compare the predicted performances to the results of an actual experimentation on parallel hardware up to 384 cores. We show that the model is accurate and predicts performance close to the empirical data. Moreover, as we study different types of instances (random and crafted), we observe that the local search solvers exhibit different behaviors and that their runtime distributions can be approximated by two types of distributions: exponential (shifted and non-shifted) and lognormal.