Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 10 / Issue 12

available in:   PDF (276 kB) PS (473 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-010-12-1629


A Signal Correlation Guided Circuit-SAT Solver

Feng Lu (University of California, USA)

Li-C. Wang (University of California, USA)

John Moondanos (Intel Corporation, USA)

Ziyad Hanna (Intel Corporation, USA)

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.

Keywords: ATPG, Boolean equivalence checking, Boolean satisfiability

Categories: B.7.2