Comparison of knowledge sharing strategies in a parallel QBF solver

In this paper we examine the effect that different knowledge sharing strategies have on the performance of our parallel QBF Solver PaQuBE. This new Master/Slave MPI based solver leverages the additional computational power that can be exploited from modern computer and system architectures, to solve more relevant instances and faster than previous generation solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential that we optimize not only which information is shared, but how it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method works best. Additionally, compression of solution cubes was explored which reduced the system time associated with message passing while also reducing network traffic.