Hardware/Software Co-modeling of SAT Solver Based on Distributed Computing Elements using SystemC

We propose the architecture of a novel distributed SAT solver, which is composed of a control unit (CU) and multiple implication units (IU). In this model, CU handles the control-intensive tasks such as clause partitioning, decision and backtracking, and IUs process implications, which are computation-intensive. This model has been modeled with SystemC successfully and simulation results show that it has the potential to get>35 speedup compared to software solvers, and moreover, it doesn’t need to re-compile implication circuits for different instances, in contrast to other hardware SAT solvers. 1