Solving Satisfiability Problems on FPGAs Using Experimental Unit Propagation Heuristic

摘要

This paper presents new resutls on an approach for solving satisfiability problems, that is, creating a logic circuit that is specialized to solve each problem instance on Field programmable gate Arrays. This approach has become feasible due to recent advances in Reconfigurable computing. We develop an algorithm that is suitable for a logic circuit implementation. This algorithm is basically equivatlent to the Davis-Putnam procedure with Experimental Unit Propagation. The required hardware resources for the algorithm are less than those of MOM's heuristics.