TS
T.C.R. Schmidt
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
Understanding SMT Solvers
Exploring Parallelization in Floating-Point Problems
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.
...
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.