Description

The hundreds of stream cores in the latest graphics processors (GPUs), and the possibility to execute non-graphics computations on them, open unprecedented levels of parallelism at a very low cost. In the last 6 years, GPUs had an increasing performance advantage of an order of magnitude relative to x86 CPUs. Furthermore, this performance advantage will continue to increase in the next 20 years because of the scalability of the chip manufacturing processes. The goal of this project is to efficiently exploit the GPU parallelism in order to accelerate the execution of a Boolean Satisfiability (SAT) solver. SAT has a wide range of applications, including formal verification and testing of software and hardware, scheduling and planning, cryptanalysis, and detection of security vulnerabilities and malicious intent in software. We bring a tremendous expertise in SAT solving, formal verification, and solving of Constraint Satisfaction Problems (CSPs) by efficient translation to SAT. In our previous work (done on the expenses of our company) we achieved 2 orders of magnitude speedup in solving Boolean formulas from formal verification of complex pipelined microprocessors, 4 orders of magnitude speedup in SAT-based solving of CSPs, and 8 orders of magnitude speedup in SAT-based routing of optical networks. During Phase 1 we implemented a prototype of a parallel GPU-based SAT solver that is 1 2 orders of magnitude faster than the best sequential SAT solvers. In Phase 2, we will continue to exploit the GPU parallelism to accelerate SAT solving, and expect to achieve speedup of 3 4 orders of magnitude.

General Information

• This data is described at

  http://catalog.data.gov/dataset/an-efficient-parallel-sat-solver-exploiting-multi-core-environments-project-ddb53 Do you think this data is incorrect? Let us know

• This data is published by

  National Aeronautics and Space Administration Do you think this data is incorrect? Let us know

Legal Information

• The rights statement is at

  http://catalog.data.gov/dataset/an-efficient-parallel-sat-solver-exploiting-multi-core-environments-project-ddb53 Do you think this data is incorrect? Let us know

• Outside the US, this data is available under

  Creative Commons CCZero Do you think this data is incorrect? Let us know

• There are

  yes, and the rights are all held by the same person or organisation Do you think this data is incorrect? Let us know

• The content is available under

  Creative Commons CCZero Do you think this data is incorrect? Let us know

• The rights statement includes data about

  its data licence Do you think this data is incorrect? Let us know

• This data contains

  no data about individuals Do you think this data is incorrect? Let us know

Practical Information

• The data appears in this collection

  http://catalog.data.gov/organization/nasa-gov Do you think this data is incorrect? Let us know

• The accuracy or relevance of this data will

  go out of date but it is timestamped Do you think this data is incorrect? Let us know

• The data is

  backed up offsite Do you think this data is incorrect? Let us know

Technical Information

• This data is published at

  http://techport.nasa.gov/xml-api/8708 Do you think this data is incorrect? Let us know

• This data is

  machine-readable Do you think this data is incorrect? Let us know

• The format of this data is

  a standard open format Do you think this data is incorrect? Let us know

Social Information

• The documentation includes machine-readable data for

  title Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  description Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  identifier Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  landing page Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  publisher Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  keyword(s) or tag(s) Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  distribution(s) Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  release date Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  modification date Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  temporal coverage Do you think this data is incorrect? Let us know

• The documentation includes machine-readable data for

  language Do you think this data is incorrect? Let us know

• The documentation about each distribution includes machine-readable data for

  release date Do you think this data is incorrect? Let us know

• The documentation about each distribution includes machine-readable data for

  a URL to access the data Do you think this data is incorrect? Let us know

• The documentation about each distribution includes machine-readable data for

  a URL to download the dataset Do you think this data is incorrect? Let us know

• The documentation about each distribution includes machine-readable data for

  type of download media Do you think this data is incorrect? Let us know

• Find out how to contact someone about this data at

  http://catalog.data.gov/dataset/an-efficient-parallel-sat-solver-exploiting-multi-core-environments-project-ddb53 Do you think this data is incorrect? Let us know

• Find out how to suggest improvements to publication at

  http://www.data.gov/issue/?media_url=http://catalog.data.gov/dataset/an-efficient-parallel-sat-solver-exploiting-multi-core-environments-project-ddb53 Do you think this data is incorrect? Let us know