Reducing Compilation Time of Zhong's FPGA-Based SAT Solver
FCCM(1999)
摘要
We present schemes to reduce the compilation time of configurable hardware that solves Boolean Satisfiability. The SAT solver presented by Zhong et al in FCCM98 has a large compilation time overhead mainly due to placement and routing of many FPGAs. We attack the problem on 3 fronts. First, we partitioning the SAT solver into instance-specific and instance non-specific components. Secondly, we transform SAT instances to canonical forms; and finally we present a board-level multiple-chip architecture to solve large SAT instances. All these efforts amount to a reduction in placement and routing time to configure the configurable hardware. We are able to reduce the compilation time to mere routing time of the implication circuits for each instance of the SAT problem, given the best scenario.
更多查看译文
关键词
instance non-specific component,large compilation time overhead,large sat instance,sat problem,mere routing time,compilation time,sat solver,sat instance,present scheme,fpga-based sat solver,configurable hardware,sun,engines,field programmable gate arrays,finite state machines,boolean satisfiability,computability,hardware,canonical forms,circuits,boolean algebra,automatic control,degradation,network routing,canonical form,routing
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络