SAT en Parallèle
Type de document :
Thèse
Titre :
SAT en Parallèle
Titre en anglais :
SAT Parallel Computing
Auteur(s) :
Szczepanski, Nicolas [Auteur]
Centre de Recherche en Informatique de Lens [CRIL]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Centre de Recherche en Informatique de Lens [CRIL]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Directeur(s) de thèse :
Gilles Audemard
Jean-Marie Lagniez (co-encadrant)
Sébastien Tabary (co-encadrant)
Jean-Marie Lagniez (co-encadrant)
Sébastien Tabary (co-encadrant)
Date de soutenance :
2017-12-12
Président du jury :
Chu-Min Li
Gilles Dequen
Thi-Bich-Hanh Dao
Gilles Dequen
Thi-Bich-Hanh Dao
Membre(s) du jury :
Chu-Min Li
Gilles Dequen
Thi-Bich-Hanh Dao
Gilles Dequen
Thi-Bich-Hanh Dao
Organisme de délivrance :
Université d'Artois
Mot(s)-clé(s) :
SAT
solveurs SAT
parallèle
calcul distribué
modèles de programmation hybride
solveurs SAT
parallèle
calcul distribué
modèles de programmation hybride
Mot(s)-clé(s) en anglais :
SAT
SAT solvers
parallel
distributed computing
hybrid programming models
SAT solvers
parallel
distributed computing
hybrid programming models
Discipline(s) HAL :
Informatique [cs]/Calcul parallèle, distribué et partagé [cs.DC]
Résumé :
La thèse porte sur la résolution des problèmes de satisfaisabilité booléenne (SAT) dans un cadre massivement parallèle. Le problème SAT est largement utilisé pour résoudre des problèmes combinatoires de première importance ...
Lire la suite >La thèse porte sur la résolution des problèmes de satisfaisabilité booléenne (SAT) dans un cadre massivement parallèle. Le problème SAT est largement utilisé pour résoudre des problèmes combinatoires de première importance comme la vérification formelle de matériels et de logiciels, la bio-informatique, la cryptographie, la planification et l’ordonnancement de tâches. Plusieurs contributions sont apportées dans cette thèse. Elles vont de la conception d’algorithmes basés sur les approches « portfolio » et « diviser pour mieux régner », à l’adaptation de modèles de programmation parallèle, notamment hybride (destinés à des architectures à mémoire partagée et distribuée), à SAT, en passant par l’amélioration des stratégies de résolution. Ce travail de thèse a donné lieu à plusieurs contributions dans des conférences internationales du domaine ainsi qu’à plusieurs outils (open sources) de résolution des problèmes SAT, compétitifs au niveau international.Lire moins >
Lire la suite >La thèse porte sur la résolution des problèmes de satisfaisabilité booléenne (SAT) dans un cadre massivement parallèle. Le problème SAT est largement utilisé pour résoudre des problèmes combinatoires de première importance comme la vérification formelle de matériels et de logiciels, la bio-informatique, la cryptographie, la planification et l’ordonnancement de tâches. Plusieurs contributions sont apportées dans cette thèse. Elles vont de la conception d’algorithmes basés sur les approches « portfolio » et « diviser pour mieux régner », à l’adaptation de modèles de programmation parallèle, notamment hybride (destinés à des architectures à mémoire partagée et distribuée), à SAT, en passant par l’amélioration des stratégies de résolution. Ce travail de thèse a donné lieu à plusieurs contributions dans des conférences internationales du domaine ainsi qu’à plusieurs outils (open sources) de résolution des problèmes SAT, compétitifs au niveau international.Lire moins >
Résumé en anglais : [en]
This thesis deals with propositional satisfiability (SAT) in a massively parallel setting. The SAT problem is widely used for solving several combinatorial problems (e.g. formal verification of hardware and software, ...
Lire la suite >This thesis deals with propositional satisfiability (SAT) in a massively parallel setting. The SAT problem is widely used for solving several combinatorial problems (e.g. formal verification of hardware and software, bioinformatics, cryptography, planning, scheduling, etc.). The first contribution of this thesis concerns the design of efficient algorithms based on the approaches « portfolio » and « divide and conquer ». Secondly, an adaptation of several parallel programming models including hybrid (parallel and distributed computing) to SAT is proposed. This work has led to several contributions to international conferences and highly competitive distributed SAT solvers.Lire moins >
Lire la suite >This thesis deals with propositional satisfiability (SAT) in a massively parallel setting. The SAT problem is widely used for solving several combinatorial problems (e.g. formal verification of hardware and software, bioinformatics, cryptography, planning, scheduling, etc.). The first contribution of this thesis concerns the design of efficient algorithms based on the approaches « portfolio » and « divide and conquer ». Secondly, an adaptation of several parallel programming models including hybrid (parallel and distributed computing) to SAT is proposed. This work has led to several contributions to international conferences and highly competitive distributed SAT solvers.Lire moins >
Langue :
Français
Collections :
Source :
Fichiers
- https://hal.archives-ouvertes.fr/tel-02979325/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/tel-02979325/document
- Accès libre
- Accéder au document
- https://hal.archives-ouvertes.fr/tel-02979325/document
- Accès libre
- Accéder au document
- SATenParalleleSzczepanskiNicolas.pdf
- Accès libre
- Accéder au document
- document
- Accès libre
- Accéder au document