Small Business Innovation Research/Small Business Tech Transfer
An Efficient Parallel SAT Solver Exploiting Multi-Core Environments
Project 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.
More »
Anticipated Benefits
The potential non-NASA commercial applications include: 1) Formal verification and testing of software and hardware, where the potential customers will be all major semiconductor and software companies. 2) Scheduling, planning, and solving of Constraint Satisfaction Problems (CSPs), where the potential customers will be all companies that use scheduling and planning tools. 3) Electronic Design Automation (EDA) problems, such as FPGA technology mapping and routing, power consumption analysis for circuits, and formal methods to check the robustness of radiation-hardened circuits, where the potential customers will be all EDA and semiconductor companies. 4) Formal methods for cryptanalysis, where the potential customers will be the Department of Defense, the NSA, and all companies that use cryptanalysis. 5) Formal methods for cyber security, such as for detection of security vulnerabilities and malicious intent in software, where the potential customers will be all companies that develop robust virus scanners based on formal methods, and companies that develop formal methods for detecting security vulnerabilities in software. Because of the potential for a very wide range of software obfuscations that can be used to hide malicious intent, future virus scanners will have to employ efficient formal methods to detect malware, and thus the importance of speed and scalability that will be possible with an efficient SAT solver.
Efficiently solving of challenging Boolean formulas is critical to NASA, as this will increase both the speed and scalability of the following applications: 1) formal verification and testing methods for complex mission software and hardware, including those of the Crew Exploration Vehicle (CEV), the next generations of Mars Rovers, and other spacecraft; 2) formal methods to check the robustness of radiation-hardened circuits; 3) SAT-based methods for scheduling, planning, and solving of other Constraint Satisfaction Problems (CSPs); 4) formal methods for network coding that will increase both the bandwidth and reliability of space communications by using the existing communications equipment that is already deployed in space after updating the firmware; 5) SAT methods for reliability-based optimization of hardware, software, and mechanical systems; 6) power consumption analysis for circuits; 7) design of experiments; 8) design of error-correction codes; and 9) FPGA technology mapping and routing. More »
Efficiently solving of challenging Boolean formulas is critical to NASA, as this will increase both the speed and scalability of the following applications: 1) formal verification and testing methods for complex mission software and hardware, including those of the Crew Exploration Vehicle (CEV), the next generations of Mars Rovers, and other spacecraft; 2) formal methods to check the robustness of radiation-hardened circuits; 3) SAT-based methods for scheduling, planning, and solving of other Constraint Satisfaction Problems (CSPs); 4) formal methods for network coding that will increase both the bandwidth and reliability of space communications by using the existing communications equipment that is already deployed in space after updating the firmware; 5) SAT methods for reliability-based optimization of hardware, software, and mechanical systems; 6) power consumption analysis for circuits; 7) design of experiments; 8) design of error-correction codes; and 9) FPGA technology mapping and routing. More »
Primary U.S. Work Locations and Key Partners
| Organizations Performing Work | Role | Type | Location |
|---|---|---|---|
| Aries Design Automation, LLC | Lead Organization | Industry | Chicago, Illinois |
Ames Research Center
(ARC)
|
Supporting Organization | NASA Center | Moffett Field, California |
Primary U.S. Work Locations
-
California
-
Illinois
Suggest an Edit
Recommend changes and additions to this project record.