HordeSat：一种大规模并行组合式 SAT 求解器
计算机科学中的逻辑
2015-08-04 v2
摘要
并行可满足性（SAT）求解的一个简单而成功的方法是同时运行多个不同的（一组）SAT求解器（portfolio）在输入问题上，直到其中一个求解器找到解。组合中的SAT求解器可以是具有不同配置设置的单个求解器的实例。此外，求解器通常可以以子句的形式交换信息。在本文中，我们研究这种方法是否适用于大规模并行SAT求解的情况。我们的求解器旨在运行在具有数千个处理器的集群上，因此命名为HordeSat。HordeSat是一个完全分布式的基于组合式的SAT求解器，具有模块化设计，允许其使用任何实现了给定接口的SAT求解器。HordeSat具有去中心化设计，并具有带交错通信和搜索的层次并行特征。我们使用2011年和2014年国际SAT竞赛应用赛道的全部基准问题对其进行了实验评估。实验表明，HordeSat可扩展至数百甚至数千个处理器，实现了显著的加速，特别是对于困难实例。
引用
@article{arxiv.1505.03340,
title = {HordeSat: A Massively Parallel Portfolio SAT Solver},
author = {Tomas Balyo and Peter Sanders and Carsten Sinz},
journal= {arXiv preprint arXiv:1505.03340},
year = {2015}
}
备注
Accepted for SAT 2015