A scalable, loadable custom programmable logic device for solving Boolean satisfiability problems
- 11 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
This paper introduces ELVIS, a custom PLD that solves Boolean satisfiability (SAT) problems and presents a significant improvement over previous approaches. SAT is a core computer science problem with important commercial applications, which include timing verification, automated layout, logic minimization and test pattern generation. ELVIS is the first massively parallel SAT-solver to support efficient loading of formulas and on-line clause addition with no instance-specific placement or routing. Furthermore, ELVIS requires significantly less hardware capacity than previous approaches. The design is easily scaled; it requires hardware that grows linearly with formula size. As such, it is the first to guarantee polynomial space and time complexity of formula loading. This avoids the laborious (NP-hard) placement and routing of each formula that has plagued previous approaches. The new approach can efficiently support dynamic clause addition, formula partitioning, implication heuristics and an unbounded number of variables per clause. Large scale implementation of these optimizations and modifying ELVIS to realize a multi-chip board design are the goals of future research.Keywords
This publication has 17 references indexed in Scilit:
- Reducing compilation time of Zhong's FPGA-based SAT solverPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- 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
- Dynamic circuit generation for solving specific problem instances of Boolean satisfiabilityPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Satisfiability-based layout revisitedPublished by Association for Computing Machinery (ACM) ,1999
- Partitioning methods for satisfiability testing on large formulasPublished by Springer Nature ,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
- Logic Minimization Algorithms for VLSI SynthesisPublished by Springer Nature ,1984
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960