Hardware Acceleration for Boolean Satisfiability Solver by Applying Belief Propagation Algorithm

TL;DR

This paper introduces a hardware-accelerated SAT solver using a belief propagation algorithm inspired by error-correcting code decoding, achieving significant speedups over traditional solvers.

Contribution

It presents a novel belief propagation-based algorithm and hardware design for SAT solving, demonstrating substantial performance improvements.

Findings

At least 30x speedup compared to MiniSat.

Time complexity remains stable regardless of SAT problem size.

Hardware acceleration effectively enhances SAT solver performance.

Abstract

Boolean satisfiability (SAT) has an extensive application domain in computer science, especially in electronic design automation applications. Circuit synthesis, optimization, and verification problems can be solved by transforming original problems to SAT problems. However, the SAT problem is known as NP-complete, which means there is no efficient method to solve it. Therefore, an efficient SAT solver to enhance the performance is always desired. We propose a hardware acceleration method for SAT problems. By surveying the properties of SAT problems and the decoding of low-density parity-check (LDPC) codes, a special class of error-correcting codes, we discover that both of them are constraint satisfaction problems. The belief propagation algorithm has been successfully applied to the decoding of LDPC, and the corresponding decoder hardware designs are extensively studied. Therefore, we proposed a belief propagation based algorithm to solve SAT problems. With this algorithm, the SAT solver can be accelerated by hardware. A software simulator is implemented to verify the proposed algorithm and the performance improvement is estimated. Our experiment results show that time complexity does not increase with the size of SAT problems and the proposed method can achieve at least 30x speedup compared to MiniSat.