Deterministic Parallel MaxSAT Solving
Deterministic Parallel MaxSAT Solving
复制标题
DOI：
10.1142/s0218213015500050
复制
发表时间：
2015-06-01
影响因子：
1.1
通讯作者：
Lynce, Ines
中科院分区：
文献类型：
--
作者：
Martins, Ruben;Manquinho, Vasco;Lynce, Ines
多核处理器正在成为当今的主导平台。因此，并行最大可满足性（MaxSAT）求解器已开发利用这种新的架构。然而，并行MaxSAT求解器遭受非确定性行为，即相同求解器的几次运行可能导致不同的解决方案。对于需要多次解决同一问题实例的应用程序来说，这是一个明显的缺点。本文提出了第一个确定性并行MaxSAT求解器，确保结果的再现性。实验结果表明，新的确定性求解器的性能与相应的非确定性版本相媲美。使用确定性求解器的另一个优点是，人们可以很容易地观察到来自不同技术的增益，因为非确定性从求解器中删除。例如，在并行MaxSAT中共享学习的子句有望有助于进一步修剪搜索空间并提高并行求解器的性能。然而，到目前为止，还没有明确哪些习得子句应该在不同线程之间共享。通过使用确定性求解器，我们提出了一个比较显示，共享学习条款提高了并行MaxSAT求解器的整体性能。
Multicore processors are becoming the dominant platform in modern days. As a result, parallel Maximum Satisfiability (MaxSAT) solvers have been developed to exploit this new architecture. However, parallel MaxSAT solvers suffer from non-deterministic behavior, i.e. several runs of the same solver can lead to different solutions. This is a clear downside for applications that require solving the same problem instance more than once. This paper presents the first deterministic parallel MaxSAT solver that ensures reproducibility of results. Experimental results show that the performance of the new deterministic solver is comparable to the corresponding non-deterministic version.Another advantage of using a deterministic solver is the fact that one can easily observe the gains coming from different techniques, since the non-determinism is removed from the solver. For example, sharing learned clauses in parallel MaxSAT is expected to help to further prune the search space and boost the performance of a parallel solver. Yet, so far it has not been made clear which learned clauses should be shared among the different threads. By using the deterministic solver, we present a comparison showing that sharing learned clauses improves the overall performance of parallel MaxSAT solvers.