A bitstream reconfigurable FPGA implementation of the WSAT algorithm

A field programmable gate array (FPGA) implementation of a coprocessor whic h uses the WSAT algorithm to solve Boolean satisfiability problems is prese nted. The input Is a SAT problem description file from which a software pro gram directly generates a problem-specific circuit design which can be down loaded to a Xilinx Virtex FPGA device and executed to find a solution. On a n XCV300, problems of 50 variables and 170 clauses can be solved. Compared with previous approaches, it avoids the need for resynthesis, placement, an d routing for different constraints. Our coprocessor is eminently suitable for embedded applications where energy, weight and real-time response are o f concern.