View in EDS PDF Full Text

Parallelizing simplex within SMT solvers.

Saved in:
Bibliographic Details
Title: Parallelizing simplex within SMT solvers.
Authors: Banković, Milan1 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
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 122761950
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Parallelizing simplex within SMT solvers.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Banković%2C+Milan%22">Banković, Milan</searchLink><relatesTo>1</relatesTo><i> milan@matf.bg.ac.rs</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Artificial+Intelligence+Review%22">Artificial Intelligence Review</searchLink>. Jun2017, Vol. 48 Issue 1, p83-112. 30p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Surface+mount+technology%22">Surface mount technology</searchLink><br /><searchLink fieldCode="DE" term="%22Parallelizing+compilers%22">Parallelizing compilers</searchLink><br /><searchLink fieldCode="DE" term="%22Algorithms%22">Algorithms</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+optimization%22">Mathematical optimization</searchLink><br /><searchLink fieldCode="DE" term="%22Computational+complexity%22">Computational complexity</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=122761950
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10462-016-9495-5
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 30
        StartPage: 83
    Subjects:
      – SubjectFull: Surface mount technology
        Type: general
      – SubjectFull: Parallelizing compilers
        Type: general
      – SubjectFull: Algorithms
        Type: general
      – SubjectFull: Mathematical optimization
        Type: general
      – SubjectFull: Computational complexity
        Type: general
    Titles:
      – TitleFull: Parallelizing simplex within SMT solvers.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Banković, Milan
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2017
              Type: published
              Y: 2017
          Identifiers:
            – Type: issn-print
              Value: 02692821
          Numbering:
            – Type: volume
              Value: 48
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Artificial Intelligence Review
              Type: main
ResultId 1