Deterministic Parallel DPLL
Deterministic Parallel DPLL
复制标题
确定性并行 DPLL
DOI：
10.3233/sat190081
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
L. Sais
中科院分区：
文献类型：
--
作者：
Y. Hamadi;Saïd Jabbour;Cédric Piette;L. Sais
当前的并行SAT求解器存在不确定性行为。这是他们的体系结构依赖于弱同步来最大化性能的结果。对于习惯于运行时和解决方案可再现性的从业者来说，这种行为是一个明显的缺点。在本文中，我们提出了第一个确定性并行DPLL引擎。我们的实验结果清楚地表明，我们的方法保留了并行投资组合方法的性能，同时确保了结果的完全可重复性。
Current parallel SAT solvers suer from a non-deterministic behavior. This is the consequence of their architectures which rely on weak synchronizing in an attempt to maximize performance. This behavior is a clear downside for practitioners, who are used to both runtime and solution reproducibility. In this paper, we propose the rst Deterministic Parallel DPLL engine. Our experimental results clearly show that our approach preserves the performance of the parallel portfolio approach while ensuring full reproducibility of the results.