文章基本信息

标题：A Signal Correlation Guided Circuit-SAT Solver
本地全文：下载
作者：F. Lu ; L.-C. Wang ; J. Moondanos 等
期刊名称：Journal of Universal Computer Science
印刷版ISSN：0948-6968
出版年度：2004
卷号：10
期号：12
DOI：10.3217/jucs-010-12-1629
出版社：Graz University of Technology and Know-Center
摘要：We propose two heuristics, implicit learning and explicit learning, that utilize circuit topological information and signal correlations to derive conflict clauses that could efficiently prune the search space for solving circuit based SAT problem instances. We implemented a circuit-SAT solver SC-C-SAT based on the proposed heuristics and the concepts used in other state-of-the-art SAT solvers. For solving unsatisfiable circuit examples and for solving difficult circuit-based problems at Intel, our solver is able to achieve speedup of one order of magnitude over other state-of-the-art SAT solvers that do not use the heuristics.
关键词：ATPG, Boolean equivalence checking, Boolean satisfiability