An architecture for solving boolean satisfiability using runtime configurable hardware

An architecture is proposed for a forward checking tree search which is used for solving satisfiability problems. In this design, the FPGA on-chip RAM feature is used to achieve a large improvement in density over a straightforward implementation using configurable logic blocks, enabling much larger problems to be solved. In addition, the boolean function to be satisfied is runtime configurable. A prototype implementation of the design operated successfully at 10 MHz for a 50 variable, 80 clause 3-SAT problem