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-a