A simple yet successful approach to parallel satisfiability (SAT) solving is
to run several different (a portfolio of) SAT solvers on the input problem at
the same time until one solver finds a solution. The SAT solvers in the
portfolio can be instances of a single solver with different configuration
settings. Additionally the solvers can exchange information usually in the form
of clauses. In this paper we investigate whether this approach is applicable in
the case of massively parallel SAT solving. Our solver is intended to run on
clusters with thousands of processors, hence the name HordeSat. HordeSat is a
fully distributed portfolio-based SAT solver with a modular design that allows
it to use any SAT solver that implements a given interface. HordeSat has a
decentralized design and features hierarchical parallelism with interleaved
communication and search. We experimentally evaluated it using all the
benchmark problems from the application tracks of the 2011 and 2014
International SAT Competitions. The experiments demonstrate that HordeSat is
scalable up to hundreds or even thousands of processors achieving significant
speedups especially for hard instances.

本研究探讨了在大规模并行 SAT 问题求解中应用基于投资组合的分布式 SAT 求解方法，并实现了一个名为 HordeSat 的可扩展的并行 SAT 求解器，其使用分层并行和分布式设计，实现了数百到数千个处理器的可观加速效果。