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 does not need to re-compile implication circuits for different instances, in contrast to other hardware SAT solvers.