Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel - Université de Lorraine Access content directly
Theses Year : 2018

Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering

Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel

Abstract

In this thesis, we address a topic in the field of industrial engineering related to solving a fundamental decision problem in the theory of complexity and propositional satisfiability called SAT. The latter is usually presented in a mathematical formalism, allowing the modelling of complex problems, both academic and from real world. These problems are presented in boolean form in order to check their feasibility. They relate to several application areas, such as hardware and software verification, telecommunications, medicine, and planning. The evolution and progress observed in recent years in the field of problem-solving using SAT has made it possible to reinforce the conviction that this field can be even more promising in solving difficult (complex or complex NP) problems and that more attention needs to be dedicated to it. It is with this in mind that we have taken an interest in applying it to purely industrial problems in order to propose contributions in a new field of application. The objective of this thesis is to develop decision-support tools that can be used in the field of industrial risk management. Although the SAT formalism is very powerful, in practice, when the targeted problems are large, the resolution tools prove to be less effective. Therefore, the aim of this research is to develop a rapid hardware architecture (with FPGA-targeted implementation) that allows massive acceleration of resolution due to the high level of parallel processing of the hardware approach. In this thesis, two main aspects are studied and developed to solve a problem of management of industrial production resources. These aspects are, on the one hand, the basic principles of operation and resolution of a generic SAT configurable solver and, on the other hand, methods adapted to the operating principle adopted for the hardware solver. Indeed, although targeting goals comparable to those of the software approach (optimization of the search space path), the material approach requires the development of specific resolution methods. These have been specifically optimised for the target application area of industry. The effectiveness of the material approach developed showed satisfactory results, point of view of the number of variables used and resolution time on the problems tested.
Dans cette thèse, nous abordons un sujet dans le domaine du génie industriel se rapportant à la résolution d’un problème de décision, fondamental dans la théorie de la complexité et de la satisfiabilité propositionnelle, nommé SAT. Ce dernier est présenté généralement sous un formalisme mathématique, permettant de modéliser des problèmes complexes, tant académiques qu’issus du monde réel. Ces problèmes sont présentés sous une forme booléenne dans le but de tester leur faisabilité. Ils sont relatifs à plusieurs domaines applicatifs, tels que la vérification de matériels et logiciels, les télécommunications, la médecine, et notamment la planification. L’évolution et les progrès observés ces dernières années dans le domaine de la résolution des problèmes utilisant SAT, a permis de renforcer la conviction que ce domaine peut être encore plus prometteur dans la résolution des problèmes difficiles (complexes ou NP complexes) et qu’il faut lui accorder plus d’intérêt. C’est dans cette optique, que nous nous sommes intéressés à l’appliquer sur des problèmes purement industriels afin de proposer des contributions dans un nouveau domaine d’application. L’objectif de cette thèse est de développer des outils d’aide à la décision pouvant être employés dans le domaine de la gestion du risque industriel. Bien que le formalisme SAT soit très puissant, dans la pratique, quand les problèmes ciblés sont de taille importante, les outils de résolution s’avèrent moins performants. Par conséquent le but de ces travaux de recherche est de développer une architecture matérielle rapide (avec une implémentation ciblée sur FPGA) permettant une accélération massive de la résolution grâce au niveau élevé de traitement parallèle de l’approche matérielle. Dans cette thèse, deux aspects principaux sont étudiés et développés pour résoudre un problème de gestion des ressources de production industriel. Ces aspects sont d’une part, les principes de base de fonctionnement et de résolution d’un solveur générique paramétrable SAT, d’autre part, des méthodes adaptées au principe de fonctionnement retenu pour le solveur matériel. En effet, bien que ciblant des buts comparables à ceux de l’approche logicielle (optimisation du parcours de l’espace de recherche), l’approche matérielle requiert le développement de méthodes de résolutions spécifiques. Ces dernières ont été spécifiquement optimisées pour le domaine applicatif cible qui est celui de l’industrie. L’efficacité de l’approche matérielle développée a montré des résultats satisfaisant, point de vu du nombre de variables utilisés et temps de résolution sur les problèmes testés.
Fichier principal
Vignette du fichier
DDOC_T_2018_0341_BOUSMAR.pdf (1.59 Mo) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

tel-02510914 , version 1 (18-03-2020)

Identifiers

  • HAL Id : tel-02510914 , version 1

Cite

Khadija Bousmar. Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel. Sciences de l'ingénieur [physics]. Université de Lorraine, 2018. Français. ⟨NNT : 2018LORR0341⟩. ⟨tel-02510914⟩
136 View
605 Download

Share

Gmail Mastodon Facebook X LinkedIn More