SAT en Parallèle
Document type :
Thèse
Title :
SAT en Parallèle
English title :
SAT Parallel Computing
Author(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]
Thesis director(s) :
Gilles Audemard
Jean-Marie Lagniez (co-encadrant)
Sébastien Tabary (co-encadrant)
Jean-Marie Lagniez (co-encadrant)
Sébastien Tabary (co-encadrant)
Defence date :
2017-12-12
Jury president :
Chu-Min Li
Gilles Dequen
Thi-Bich-Hanh Dao
Gilles Dequen
Thi-Bich-Hanh Dao
Jury member(s) :
Chu-Min Li
Gilles Dequen
Thi-Bich-Hanh Dao
Gilles Dequen
Thi-Bich-Hanh Dao
Accredited body :
Université d'Artois
Keyword(s) :
SAT
solveurs SAT
parallèle
calcul distribué
modèles de programmation hybride
solveurs SAT
parallèle
calcul distribué
modèles de programmation hybride
English keyword(s) :
SAT
SAT solvers
parallel
distributed computing
hybrid programming models
SAT solvers
parallel
distributed computing
hybrid programming models
HAL domain(s) :
Informatique [cs]/Calcul parallèle, distribué et partagé [cs.DC]
French abstract :
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 ...
Show more >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.Show less >
Show more >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.Show less >
English abstract : [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, ...
Show more >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.Show less >
Show more >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.Show less >
Language :
Français
Collections :
Source :
Files
- https://hal.archives-ouvertes.fr/tel-02979325/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/tel-02979325/document
- Open access
- Access the document
- https://hal.archives-ouvertes.fr/tel-02979325/document
- Open access
- Access the document
- SATenParalleleSzczepanskiNicolas.pdf
- Open access
- Access the document
- document
- Open access
- Access the document