A massively-parallel easily-scalable satisfiability solver using reconfigurable hardware
- 20 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 684-690
- https://doi.org/10.1109/dac.1999.782036
Abstract
Satisfiability (SAT) is a computationally expensive algorithm central to many CAD and test applications. 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 implementation, and with a prior SAT solver using reconfigurable hardware.Keywords
This publication has 17 references indexed in Scilit:
- Optimal layout via Boolean satisfiabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- GRASP-A new search algorithm for satisfiabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Timing analysis and delay-fault test generation using path-recursive functionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Dynamic circuit generation for solving specific problem instances of Boolean satisfiabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- 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
- Logic Minimization Algorithms for VLSI SynthesisPublished by Springer Nature ,1984
- An Implicit Enumeration Algorithm to Generate Tests for Combinational Logic CircuitsIEEE Transactions on Computers, 1981
- The complexity of theorem-proving proceduresPublished by Association for Computing Machinery (ACM) ,1971
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960