People/Web Search Calendar Emergency Info A-Z Index UVA Email University of Virginia

Computer Science Colloquia

Wednesday, April 29, 2015
Deyuan Guo
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

ABSTRACT

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.