Abstract
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 constrast to other hardware SAT solvers.