Résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle

• Directeur de thèse :
• Lakhdar Saïs

• Co-encadrant de thèse :
• Saïd Jabbour

• Financement : MSR

• Thèse soutenue le :
• 8 juil. 2013

• Accéder au document

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 la base 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.