Skip Navigation
SBIR/STTR

An Efficient Parallel SAT Solver Exploiting Multi-Core Environments, Phase I

Completed Technology Project

Project Introduction

An Efficient Parallel SAT Solver Exploiting Multi-Core Environments, Phase I
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. We will investigate ways to efficiently exploit this 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. 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 obtained 2 orders of magnitude speedup in solving Boolean formulas from formal verification of complex pipelined microprocessors, as well as 4 orders of magnitude speedup in SAT-based solving of CSPs. We expect to achieve speedups of up to 1 -- 2 orders of magnitude in Phase 1, and up to 3 -- 4 orders of magnitude in Phase 2. More »

Primary U.S. Work Locations and Key Partners

Project Library

Share this Project

Organizational Responsibility

Project Management

Project Duration

This is a historic project that was completed before the creation of TechPort on October 1, 2012. Available data has been included. This record may contain less data than currently active projects.

A final report document may be available for this project. If you would like to request it, please contact us.

^