Collaborative Research: SHF: Medium: A hardware accelerator for satisfiability (SAT): Over 100x speedup for combinatorial optimization problems

About This Grant

Boolean satisfiability (SAT) is a core problem in computing with broad, high-impact applications. A wide range of critical problems in industry and defense, e.g., in hardware and software design and verification, artificial intelligence, robotics, and drug discovery, use SAT solvers and often take weeks to complete on modern large-scale computing systems. This project will develop new types of accelerator chips custom-designed for SAT to reduce the time and energy required to solve all such important problems by more than two orders of magnitude compared to the best-known existing approaches. Completely new ways to combine logic circuits and memories will be developed, along with methods and tools to create these chips. The development of this hardware will dramatically benefit organizations across engineering, artificial intelligence, science, business, logistics, and defense. This project will also advance the art and science of custom computing, which will continue to increase in importance in the foreseeable future. Students will be trained in this new art and science. The models, methods, and tools developed will be shared with researchers as well as industry and defense experts to foster a vibrant community. The project will develop an algorithm-to-transistors co-optimization approach to accelerator design for SAT and an extensive set of combinatorial problems, demonstrating significantly higher efficiency than existing solutions. It will also provide new computer-aided design (CAD) tools for the realization of powerful SAT accelerators by mapping SAT algorithms and heuristics to optimized architectures, including combinations of memories, content-addressable memories, near-memory logic, and custom interconnects that enable maximal parallelization. The advantages of the new designs will be demonstrated via chip fabrication, silicon measurements, and the development of chiplet-based architectures enhancing the economics of accelerators for SAT and other problems. The technological advancements pursued by this project, and especially the new methods and tools for the design of hardware accelerators, will contribute to the state of the art in custom computing, which will become increasingly more important in the post-Moore era. The resulting designs will dramatically benefit organizations across engineering, artificial intelligence, science, business, logistics, and defense. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.