Exploiting Different Strategies for the Parallelization of an SMT Solver.
Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker · 2010
In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance is explored in parallel by several copies of the same solver but using different heuristics to guide the search. We also combine both approaches such that solvers examine disjoint parts of the search space using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT. 1