An Effective FPGA Solver on Probability Distribution and Preprocessing

The Boolean satisfiability (SAT) problem is the key problem in computer theory and application. A novel algorithm is introduced to implement a SLS hardware solver called probSAT+. The algorithm has no complex heuristic, and it only depends on the concepts of preprocessing technology, probability distribution and centralized search. Through constraining the initial assignments of the variables, the number of flipped variables was reduced while the solver finding a solution. Moreover, the algorithm no longer adopts some non-continuous if-then-else decisions, but depends on a single continuous function f(x,v). The flipping probability is not obtained by complex calculations, instead being selected by looking up tables, which effectively improves the performance of the solver. As far as we know, the probability distribution selection strategy descripted by hardware description language is firstly adopted by hardware SAT solver, which can be easily transplanted to any programmable logic device. The experimental results show that the probSAT+ solver is generally lower than the advanced software solver in the number of flips (up to 9.8 × 10 6 ), and the speedup is approximately 2.6 times with single thread, which shows that the probSAT+ has better results with fewer variables flipping times when a solution can be found. In addition, the success ratio of the solver in finding a solution of the problem in a suitable time is 100%.