Understanding SMT Solvers
Exploring Parallelization in Floating-Point Problems
T.C.R. Schmidt (TU Delft - Electrical Engineering, Mathematics and Computer Science)
S.S. Chakraborty – Mentor (TU Delft - Programming Languages)
D.G. Sprokholt – Mentor (TU Delft - Programming Languages)
A.E. Zaidman – Graduation committee member (TU Delft - Software Technology)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
To solve floating-point SMT problems, a variety of algorithms can be used, but there is not one algorithm that truly stands out at solving any kind of problem, as most have their own specific subset of problems where they perform well. A solution to maintaining efficiency in solving any kind of floating-point SMT problem is to run many of these domain specific solvers in parallel, allowing the best to always come out on top. This paper aims to provide an insight into possible improvements using parallelization by running multiple solvers (in parallel) on a large and diverse set of problems. We show that by parallelizing diverse solvers we can obtain a significant speedup over individual solvers on complex problems.