Sequential and parallel resolution of the problem of propositionnal satistifiability

Cette thèse porte sur la résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle(SAT). Ce problème important sur le plan théorique admet de nombreuses applications qui vont de la vérification formelle de matériels et de logiciels à la cryptographie en passant par la planification et la bioinformatique. Plusieurs contributions sont apportées dans cette thèse. La première concerne l’étude et l’intégration des concepts d’intensification et de diversification dans les solveurs SAT parallèle de type portfolio. Notre seconde contribution exploite l’état courant de la recherche partiellement décrit par les récentes polarités des littéraux « progress saving », pour ajuster et diriger dynamiquement les solveurs associés aux différentes unités de calcul. Dans la troisième contribution, nous proposons des améliorations de la stratégie de réduction de labase des clauses apprises. Deux nouveaux critères, permettant d’identifier les clauses pertinentes pour la suite de la recherche, ont été proposés. Ces critères sont utilisés ensuite comme paramètre supplémentaire de diversification dans les solveurs de type portfolio. Finalement, nous présentons une nouvelle approche de type diviser pour régner où la division s’effectue par ajout de contraintes particulières.In this thesis, we deal with the sequential and parallel resolution of the problem SAT. Despite of its complexity, the resolution of SAT problem is an excellent and competitive approach for solving thecombinatorial problems such as the formal verification of hardware and software, the cryptography, theplanning and the bioinfomatics. Several contribution are made in this thesis. The first contribution aims to find the compromise of diversification and intensification in the solver of type portfolio. In our second contribution, we propose to dynamically adjust the configuration of a core in a portfolio parallel sat solver when it is determined that another core performs similar work. In the third contribution, we improve the strategy of reduction of the base of learnt clauses, we construct a portfolio strategy of reduction in parallel solver. Finally, we present a new approach named "Virtual Control" which is to distribute the additional constraints to each core in a parallel solver and verify their consistency during search