Reconfigurable hardware accelerator for boolean satisfiability solver
US8131660B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Apr 8, 2008 |
| Grant date | Mar 6, 2012 |
| Priority date | — |
| Expiry date | Jan 5, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06N5/04
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A hardware accelerator is provided for Boolean constraint propagation (BCP) using field-programmable gate arrays (FPGAs) for use in solving the Boolean satisfiability problem (SAT). An inference engine may perform implications. Block RAM (BRAM) may be used to store SAT instance information. Computation may be co-located with the BRAM memory, taking advantage of the high on-chip bandwidth and low latency of an FPGA. SAT instances may be partitioned into multiple groups that can be processed by multiple inference engines in parallel. New SAT instances can be inserted into FPGA without invoking the time-consuming FPGA re-synthesizing process.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.