You are here

An Efficient Parallel SAT Solver Exploiting Multi-Core Environments

Award Information
Agency: National Aeronautics and Space Administration
Branch: N/A
Contract: NNX10CA19C
Agency Tracking Number: 085391
Amount: $600,000.00
Phase: Phase II
Program: SBIR
Solicitation Topic Code: X1.02
Solicitation Number: N/A
Solicitation Year: 2008
Award Year: 2010
Award Start Date (Proposal Award Date): 2010-03-29
Award End Date (Contract End Date): 2014-08-31
Small Business Information
IL, Chicago, IL, 60660-5818
DUNS: 361627933
HUBZone Owned: N
Woman Owned: N
Socially and Economically Disadvantaged: N
Principal Investigator
 Miroslav Velev
 Principal Investigator
 (773) 856-6633
Business Contact
 Miroslav Velev
Title: Business Official
Phone: (773) 773-6633
Research Institution
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.

* Information listed above is at the time of submission. *

US Flag An Official Website of the United States Government