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.
Citation:
Jinwen Xi, Peixin Zhong, "Hardware/Software Co-Modeling of SAT Solver Based on Distributed Computing Elements using SystemC," iccd, pp.502-504, 2004 IEEE International Conference on Computer Design (ICCD'04), 2004