Parallelizing simplex within SMT solvers.

Saved in:

Bibliographic Details
Title:	Parallelizing simplex within SMT solvers.
Authors:	Banković, Milan¹ milan@matf.bg.ac.rs
Source:	Artificial Intelligence Review. Jun2017, Vol. 48 Issue 1, p83-112. 30p.
Subjects:	Surface mount technology, Parallelizing compilers, Algorithms, Mathematical optimization, Computational complexity
Abstract:	The usual approach in parallelizing SAT and SMT solvers is either to explore different parts of the search space in parallel (divide-and-conquer approach) or to run multiple instances of the same solver with suitably altered parameters in parallel, possibly exchanging some information during the solving process (parallel portfolio approach). Quite a different approach is to parallelize the execution of time-consuming algorithms that check for satisfiability and propagations during the search space exploration. Since most of the execution time is spent in these procedures, their efficient parallelization might be a promising research direction. In this paper we present our experience in parallelizing the simplex algorithm which is typically used in the SMT context to check the satisfiability of linear arithmetic constraints. We provide a detailed description of this approach and present experimental results that evaluate the potential of the approach compared to the parallel portfolio approach. We also consider the combination of the two approaches. [ABSTRACT FROM AUTHOR]
	Copyright of Artificial Intelligence Review is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database:	Engineering Source

Description
Abstract:	The usual approach in parallelizing SAT and SMT solvers is either to explore different parts of the search space in parallel (divide-and-conquer approach) or to run multiple instances of the same solver with suitably altered parameters in parallel, possibly exchanging some information during the solving process (parallel portfolio approach). Quite a different approach is to parallelize the execution of time-consuming algorithms that check for satisfiability and propagations during the search space exploration. Since most of the execution time is spent in these procedures, their efficient parallelization might be a promising research direction. In this paper we present our experience in parallelizing the simplex algorithm which is typically used in the SMT context to check the satisfiability of linear arithmetic constraints. We provide a detailed description of this approach and present experimental results that evaluate the potential of the approach compared to the parallel portfolio approach. We also consider the combination of the two approaches. [ABSTRACT FROM AUTHOR]
ISSN:	02692821
DOI:	10.1007/s10462-016-9495-5