Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | Keywords |
|---|---|---|
2004 | JOURNAL OF UNIVERSAL COMPUTER SCIENCE | Boolean Satisfiability,Boolean equivalence checking,ATPG |
Field | DocType | Volume |
Signal correlation,Topological information,Computer science,Sat problem,Boolean satisfiability problem,Theoretical computer science,Implicit learning,Heuristics,Solver,Speedup | Journal | 10 |
Issue | ISSN | Citations |
12 | 0948-695X | 3 |
PageRank | References | Authors |
0.43 | 22 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Feng Lu | 1 | 174 | 12.25 |
| Li-C. Wang | 2 | 439 | 34.93 |
| Kwang-Ting Cheng | 3 | 5755 | 513.90 |
| John Moondanos | 4 | 96 | 9.70 |
| Ziyad Hanna | 5 | 292 | 17.66 |