论文标题
可扩展的SAT在云中解决
Scalable SAT Solving in the Cloud
论文作者
论文摘要
以前在使高性能计算（HPC）解决可满足性（SAT）的努力已导致特定公式的超级线性加速，但是对于大多数输入而言，无法有效利用大量处理器。此外，长期潜伏期（几分钟到几天）的工作时间表使大规模的SAT在大多数应用中按需求解不切实际。我们解决了MALLOB的这两个问题，Mallob是SAT解决的上下文中的工作调度框架，该框架利用了锻造性，即在计算过程中从作业中添加或删除处理能力的能力。 Mallob包括基于Hordesat的大规模平行，分布式和可延展的SAT求解引擎，采用更简洁和沟通效率的方法来进行子句共享，并且对其前体进行了许多进一步的改进。例如，在640个内核上的mallob优于2560核对Hordesat的更新和改进的配置。此外，Mallob还可以在动态调整分配的资源的同时并行解决许多公式，并且到达系统中的作业通常在一秒钟内启动。
Previous efforts on making Satisfiability (SAT) solving fit for high performance computing (HPC) have lead to super-linear speedups on particular formulae, but for most inputs cannot make efficient use of a large number of processors. Moreover, long latencies (minutes to days) of job scheduling make large-scale SAT solving on demand impractical for most applications. We address both issues with Mallob, a framework for job scheduling in the context of SAT solving which exploits malleability, i.e., the ability to add or remove processing power from a job during its computation. Mallob includes a massively parallel, distributed, and malleable SAT solving engine based on Hordesat with a more succinct and communication-efficient approach to clause sharing and numerous further improvements over its precursor. For example, Mallob on 640 cores outperforms an updated and improved configuration of Hordesat on 2560 cores. Moreover, Mallob can also solve many formulae in parallel while dynamically adapting the assigned resources, and jobs arriving in the system are usually initiated within a fraction of a second.
