A Signal Correlation Guided Circuit-SAT Solver
Feng Lu, John Moondanos, Li-C. Wang, Ziyad Hanna · Zenodo (CERN European Organization for Nuclear Research) · 2020
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.