A Configurable Hardware/Software Approach to SAT Solving

This paper presents the first configware/software solution for the Boolean satisfiability problem (SAT). Our partitioning assigns the two most difficult tasks (computing implications and selecting the next decision variable) for configurable hardware (configware) implementation. Conflict diagnosis, backtrack control, and clause database management are performed in software. Our approach avoids instance-specific place and route, and features a virtual hardware scheme with context switching which allows solving problems that are larger than the configware capacity. Some preliminary results show the feasibility of the approach.