The Message-Passing Interface and Parallel SAT-Solvers
Levis Zerpa · 2017
In this paper we examine the communication aspects of parallel SAT-solving. In particular, the paper is focused on the system PMSat. Besides the algorithms and heuristics implemented in that system, PMSat implements the Message-Passing Interface, the standard for a huge range of parallel architectures. A detailed analysis of some of the source code of the system shows some interesting and non-trivial aspects of the MPI functions in the treatment of the SAT problem. Moreover, the advantage of the use of the RMA operations from MPI-2 is the possibility of taking advantage of the direct semantic matching of these functions with the RDMA operations of InfiniBand and other interconnect networks.