Circuit Solvers for Hard Problems

Aims of the project

We are investigating the use of novel hardware to solve hard problems, such as Boolean satisfiability, an NP-complete problem. Given an instance of a problem (such as 3SAT), we use software to compile the problem into a specialised digital circuit which will attempt to solve that problem instance. The circuit is then realised, and allowed to run. We have carried out a set of preliminary experiments where the circuits are programmed into standard FPGA chips, and we are also planning to design a programmable ASIC chip that would be better suited than general purpose FPGAs. The circuits that we generate make use of feedback and massive parallelism in order to explore the search space more rapidly than state machines do.

Members of the project team

We are all in the Department of Computing Science at the University of Glasgow, unless otherwise noted.

Publications


John O'Donnell, jtod@dcs.gla.ac.uk