SMPP: Generic SAT Solver over Reconfigurable Hardware Accelerator

To further exploit the potential of reconfigurable computing, fine-grain, super massive parallel processing SAT solver over reconfigurable hardware accelerator is proposed in this paper as SMPP. By analyzing the traditional SAT solver, we proposed a novel way to partition the original problem into software part and hardware part. Software part uses semi-confliction guided backtrack to extract equivalent fixed scale sub-problem sequence. Partition scheme of SMPP exploited the stage effect of inference engine in modern software SAT solver. Hardware part uses tiny processing cells to handle small scale SAT problem in linear time proportional to the number of clause. Theoretical analyze and experiment results show that the speed up factor is significant.