A scalable, loadable custom programmable logic device for solving Boolean satisfiability problems

摘要

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.