This project has concluded.

Aresty Research Assistant
A computer hardware accelerator for satisfiability and artificial intelligence
Project Summary
In computer engineering, an important way to deliver greater efficiency and performance is through specialized hardware accelerators. Such accelerators are tailored to solve specific problem types or problem instances, while trading away the ability to solve general problems. Such a scheme has been an important strategy as Moore's law and transistor scaling is increasingly costly to sustain.

Despite the promise of hardware accelerators, the matching of problem types to computer hardware remains an open area of research. The main areas in which hardware accelerators have gained widespread use are in cryptography, networks, and image processing. The key challenge is in finding broadly useful types of problems that are suitable for solution in specialized electronic circuits.

This project explores the possibility of solving the Weighted Model Counting (WMC) problem using a hardware accelerator. The WMC problem is closely related to the Boolean satisfiability problem, in that WMC first requires finding sets of Boolean variable assignments that satisfy a Boolean function. The additional step in WMC is that such sets of variable assignments is associated with a weight function, and the overall problem is to find the sum of all such weights. WMC as an abstract problem format shows up in numerous useful algorithms throughout computer science, including in artificial intelligence Bayesian networks, probabilistic algorithms, and quantum computing. It is so critically useful that there are whole competitions set up to see who has the best solver algorithm implementation:
https://mccompetition.org/

Thus far, WMC problems have been tackled in parallel CPUs, but these problems have not yet captured the attention of computer hardware researchers. It is likely that some approaches to solving WMC have straightforward implementations in specialized hardware. Such a hardware accelerator would in turn drastically boost the performance and efficiency of solving problems in AI and satisfiability.




Sign in to view more information about this project.