云环境下可扩展的 SAT 求解
分布式、并行与集群计算
2022-05-16 v1 计算机科学中的逻辑
摘要
以往使可满足性（SAT）求解适应高性能计算（HPC）的努力在特定公式上实现了超线性加速，但对大多数输入无法高效利用大量处理器。此外，作业调度的长延迟（数分钟至数天）使得大多数应用按需大规模 SAT 求解不切实际。我们通过 Mallob 解决这两个问题，这是一个在 SAT 求解背景下的作业调度框架，它利用可塑性（malleability），即作业在计算过程中增加或移除算力的能力。Mallob 包含一个基于 Hordesat 的大规模并行、分布式且可塑的 SAT 求解引擎，其对子句共享采用了更简洁且通信高效的方法，并较其前身有诸多改进。例如，Mallob 在 640 核上的表现优于配置更新改进后的 Hordesat 在 2560 核上的表现。此外，Mallob 还能在动态适配分配资源的同时并行求解多个公式，且系统中到达的作业通常在不到一秒内即被启动。
引用
@article{arxiv.2205.06590,
title = {Scalable SAT Solving in the Cloud},
author = {Dominik Schreiber and Peter Sanders},
journal= {arXiv preprint arXiv:2205.06590},
year = {2022}
}
备注
This preprint has not undergone peer review or any post-submission improvements or corrections. The Version of Record of this contribution is published in the proceedings of the International Conference on Theory and Applications of Satisfiability Testing 2021 (pp. 518-534), Springer, Cham, and is available online at https://doi.org/10.1007/978-3-030-80223-3_35