Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadatas

Cited literature [101 references]  Display  Hide  Download
Contributor : Thèses Ul <>
Submitted on : Wednesday, March 18, 2020 - 12:01:34 PM
Last modification on : Thursday, March 19, 2020 - 1:19:18 AM
Long-term archiving on: : Friday, June 19, 2020 - 1:45:55 PM


Files produced by the author(s)


  • HAL Id : tel-02510914, version 1



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⟩



Record views


Files downloads