分布式 SMT 求解的划分策略
分布式、并行与集群计算
2023-06-12 v1 计算机科学中的逻辑
摘要
对于许多可满足性模理论（Satisfiability Modulo Theories, SMT）求解器的用户而言，求解器的性能是其应用中的主要瓶颈。一种有前景的提升性能的方法是利用日益普及的并行与云计算。然而，尽管已有诸多努力，迄今为止最佳的并行方法仍由求解器组合（portfolio）构成，这意味着性能仍受限于可能的最佳顺序性能。本文中，我们重新审视用于并行 SMT 的分治方法，即将一个具有挑战性的问题划分为若干子问题。我们引入了几种新的划分策略，并在大量困难 SMT 基准测试上评估了它们单独使用以及在组合中使用的性能。我们表明，包含我们新策略的混合组合能够显著优于传统的并行 SMT 组合。
引用
@article{arxiv.2306.05854,
title = {Partitioning Strategies for Distributed SMT Solving},
author = {Amalee Wilson and Andres Noetzli and Andrew Reynolds and Byron Cook and Cesare Tinelli and Clark Barrett},
journal= {arXiv preprint arXiv:2306.05854},
year = {2023}
}
备注
Submitted to FMCAD 2023