Utilização de hardware reconfigurável para acelerar a satisfação booleana

Abstract

The paper presents a case study of accelerating Boolean satisfiability in reconfigurable hardware. Boolean satisfiability (SAT) is an important problem having many applications in CAD and other areas. We propose an application-specific approach to accelerate the backtrack search algorithm for the SAT problem formulated over discrete matrix. The algorithm employed involves a quite sophisticated control unit, which is entirely implemented in reconfigurable hardware. Finally, we analyze different possibilities of solving the SAT problem and argue that the best results can be achieved by the use of software, runningon a general-purpose computer, together with an FPGAbasedreconfigurable SAT solver.