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.