Computer Science Colloquia
Wednesday, April 29, 2015
Advisor: Kevin Skadron
Attending Faculty: Worthy Martin (Committee Chair), Gabriel Robins and Jim Cohoon
11:00 AM, Rice Hall, Rm. 242
PhD Qualifying Exam Presentation
Using the Automata Processor to Accelerate the Boolean Satisfiability Problem
We present an approach to use the Micron Automata Processor (AP) to accelerate the Boolean satisfiability problem (SAT). The SAT problem is an important problem in computer science because it is NP-complete, yet important in a wide variety of applications. This means that fast solvers are difficult to develop, but can have substantial real-world impact. The Automata Processor is a reconfigurable non-von Neumann architecture, which directly implements nondeterministic finite automata (NFA) with Booleans and counters in hardware. We hypothesize that the massive parallelism of the Automata Processor can accelerate SAT solving, and design a SAT solving approach on the AP that verifies a large number of assignments of variables in parallel by reducing the Boolean verification problem to regular expression matching. The evaluation results show that on some selected hard SAT instances, the AP solution can achieve more than 100x speedup. However, the speedup is not significant on easy SAT instances and on large instances that exceed the hardware capacity of the AP.