PBoolector: A Parallel SMT Solver for QF_BV by Combining Bit-Blasting with Look-Ahead

The development of parallel algorithms for the Satisfiability Modulo Theory (SMT) problem is a quite novel research field. Although there are already several parallel approaches for the related Satisfiability (SAT) problem out there, few implementations of parallel SMT solvers exist. In recent years parallelization has grown to an important topic throughout all fields of computer science. The clock frequency increase for new processor generations has reached a limit. Current processor generations are improved by embedding multiple cores using shared memory architecture. In this thesis a parallel SMT algorithm for the quantifier free theory of fixed-size bit-vectors (QF BV) is proposed and implemented in the tool PBoolector. The Cube and Conquer approach, which was already shown to be a successful parallel SAT solving algorithm, is lifted from bit-level to the SMT term-level. The idea of Cube and Conquer is to split a formula into independent and simpler subproblems which are solved in parallel by a sequential decision procedure. The PBoolector implementation splits a bit-vector formula and solves the subproblems in parallel with the bit-blasting procedure. The search space splitting is based on the so-called look-ahead methods. Look-ahead methods are well researched methods from the SAT area, which are adapted in this thesis for SMT bit-vector formulas. We show that the implemented algorithm can achieve clear improvements (up to super-linear speedup) on a set of hard benchmark files, which are a bottleneck for sequential SMT solvers. The formula structures for which the parallel SMT approach is appropriate will be identified and evaluated in Detail.