RECHERCHE
Architectures reconfigurables et traitement de proble`mes NP-difficiles :
un nouveau domaine d application
Youssef Hamadi
David Merceron
'
'
LIRMM, UMR 5506 CNRS/Universite´ Montpellier II
161, Rue Ada, 34392 Montpellier Cedex 5
hamadi@lirmm.fr
'''
EURIWARE, 12-14 rue du fort de St-Cyr
78067 St Quentin-en-Yvelines Cedex damercer@euriware.fr
RE´SUME´. L algorithme GSAT est un algorithme de recherche locale. Cette me´thode recherche la premie`re instanciation satisfaisable de formules logiques de forme normale conjonctive. Bien que de nature incomple`te son exploration fine de l espace de recherche associe´e a` l utilisation d heuristiques puissantes lui a permis de re´soudre des proble`mes encore inaccessibles en recherche exhaustive. De plus, le caracte`re ge´ne´rique de ses formules d entre´es lui a ouvert de larges domaines d applications (synthe`se et test de circuits, planification de taÆches, ordonnancement, vision, etc &'&'& ). Dans cette e´tude, nous pre´sentons une imple´mentation de cette me´thode sur architecture reconfigurable de type FPGA [XIL 91]. Nous poursuivons par la` le double but de permettre le traitement rapide de tre`s gros proble`mes SAT et d autoriser un traitement de type temps re´el pour les instances de tailles plus re´duites. Dans ce travail, la flexibilite´ de ce type d architecture est donc utilise´e pour re´soudre efficacement des proble`mes SAT.
ABSTRACT. 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.
MOTS-CLE´S : Architectures reconfigurables, FPGA, Proble`mes SAT, Me´thodes de recherche locale
KEY WORDS :
Reconfigurable hardware, FPGA, Problems SAT, Local search procedures
