Christian Reisenberger,
"PBoolector: A Parallel SMT Solver for QF_BV by Combining Bit-Blasting with Look-Ahead"
, in TNF Faculty of Engineering and Natural Sciences, Johannes Kepler Universität, Linz, 11-2014
Original Titel:
PBoolector: A Parallel SMT Solver for QF_BV by Combining Bit-Blasting with Look-Ahead
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-