A massively-parallel easily-scalable satisfiability solver using reconfigurable hardware
- 1 June 1999
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 684-690
- https://doi.org/10.1145/309847.310028
Abstract
Satisfiability (SAT) is a computationally expensive algorithm central to many CAD and test appli- cations. In this paper, we present the architecture of a new SAT solver using reconfigurable logic. Our main contributions include new forms of massive fine-grain parallelism and structured design techniques based on iterative logic arrays that reduce compilation times from hours to a few minutes. Our architecture is easily scalable. Our results show several orders of magnitude speed-up compared with a state-of-the-art software implementa- tion, and with a prior SAT solver using reconfigurable hardware.Keywords
This publication has 7 references indexed in Scilit:
- Satisfiability-based layout revisitedPublished by Association for Computing Machinery (ACM) ,1999
- Using reconfigurable computing techniques to accelerate problems in the CAD domainPublished by Association for Computing Machinery (ACM) ,1998
- Combinational test generation using satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1996
- Asynchronous circuit synthesis with Boolean satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1995
- Test pattern generation using Boolean satisfiabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1992
- The complexity of theorem-proving proceduresPublished by Association for Computing Machinery (ACM) ,1971
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960