Architectures reconfigurables et traitement de problèmes NP-difficiles : un nouveau domaine d’application

  • Youssef Hamadi

Revue Techniques et Sciences Informatiques (TSI) |

GSAT is a greedy local search procedure. It searches for satisfiable instanciations of formulas under conjunctive normal form. Intrinsically incomplete, this algorithm has shown its ability to deal with formulas of large size that are not yet accessible to exhaustive methods. Many problems such as circuits synthesis and test, planning, scheduling, vision can efficiently be solved by using the GSAT algorithm. In this study, we give an implementation of GSAT on Field Programmable Gate Arrays (FPGA) [XIL 91] in order to speed-up the resolution of SAT problems. By this implementation, our aim is to reach very large SAT problems and to enable real-time resolution for current size problems. The FPGA technology allows users to adapt a generic logic chip to different tasks. In the framework of SAT problems we show how to quickly adapt our chips to efficiently solve satisfiability problems.