Summary
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.
