A circuit SAT solver with signal correlation guided learning

Boolean Satisfiability has attracted tremendous research effort in recent years, resulting in the developments of various efficient SAT solver packages. Based upon their design architectures, researchers have tried to develop better heuristics to further improve its efficiency, by either speeding up the Boolean Constraint Propagation (BCP) procedure or finding a better decision ordering (or both). In this paper, we propose an entirely different SAT solver design concept that is circuit-based. Our solver is able to utilize circuit topological information and signal correlations to enforce a decision ordering that is more efficient for solving circuit-based SAT problem instances. In particular, for unsatisfiable circuit examples, our solver is able to achieve from 2x up to more than 75x speedup over a state-of-the-art SAT solver.