Incorporating Learning in Grid-Based Randomized SAT Solving
Incorporating Learning in Grid-Based Randomized SAT Solving
复制标题
将学习融入基于网格的随机 SAT 求解
DOI：
10.1007/978-3-540-85776-1_21
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
I. Niemelä
中科院分区：
文献类型：
--
作者：
A. Hyvärinen;Tommi A. Junttila;I. Niemelä
计算网格提供了适合随机 SAT 求解的广泛分布式计算环境。本文开发了将学习结合起来的技术，已知这些技术可以在这种分布式框架中在顺序情况下产生显着的加速。该方法利用现有最先进的子句学习 SAT 求解器，几乎无需任何修改即可嵌入它们。我们表明，对于许多工业 SAT 实例，通过仔细组合分布式求解器的学习子句可以减少预期运行时间。我们通过使用一组有代表性的基准来比较不同的并行学习策略，并利用结果设计一种在网格环境中学习增强的随机 SAT 求解算法。最后，我们在生产级网格中对该算法的实现进行了实验，并解决了 SAT 2007 求解器竞赛中未解决的几个问题。
Computational Grids provide a widely distributed computing environment suitable for randomized SAT solving. This paper develops techniques for incorporating learning, known to yield significant speed-ups in the sequential case, in such a distributed framework. The approach exploits existing state-of-the-art clause learning SAT solvers by embedding them with virtually no modifications. We show that for many industrial SAT instances, the expected run time can be decreased by carefully combining the learned clauses from the distributed solvers. We compare different parallel learning strategies by using a representative set of benchmarks, and exploit the results to devise an algorithm for learning-enhanced randomized SAT solving in Grid environments. Finally, we experiment with an implementation of the algorithm in a production level Grid and solve several problems which were not solved in the SAT 2007 solver competition.