A software/reconfigurable hardware SAT solver

Abstract—This paper introduces a novel approach for solving the Boolean satisfiability (SAT) problem by combining software and configurable hardware. The suggested technique avoids in-stance-specific hardware compilation and, as a result, allows the total problem solving time to be reduced compared to other ap-proaches that have been proposed. Moreover, the technique per-mits problems that exceed the resources of the available reconfig-urable hardware to be solved. The paper presents the results ob-tained with some of the DIMACS benchmarks and a comparison of our implementation with other available SAT solvers based on reconfigurable hardware. The hardware part of the satisfier was realized on Virtex XCV812E FPGA, which has a large volume of embedded memory blocks that provide direct support for the pro-posed approach. Index Terms—Boolean satisfiability, configurable computing, field-programmable gate array (FPGA), partitioning. I