Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel

Monnet, Anthony Jean-Luc (2013). « Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel » Thèse. Montréal (Québec, Canada), Université du Québec à Montréal, Doctorat en informatique.

Fichier(s) associé(s) à ce document :
[img]
Prévisualisation
PDF
Télécharger (27MB)

Résumé

Cette thèse s'intéresse à l'amélioration des performances pratiques de l'algorithme CDCL (Conftict-Driven Clause Learning) pour la résolution du problème de satisfaisabilité des formules propositionnelles, ou problème SAT. Plus particulièrement, nous cherchons à diminuer la destruction de l'instanciation courante lors des étapes de saut arrière, qui peuvent occasionner la désinstanciation de nombreuses variables n'ayant aucun rapport direct avec le conflit à résoudre. Dans ce but, nous proposons trois approches différentes. La première est une amélioration de l'utilisabilité de la méthode déjà existante de décomposition implicite d'une instance SAT. Notre but principal est de permettre son application à des instances de plus grande taille possible, après avoir montré les limitations des implémentations existantes. Nous développons également deux variations de l'algorithme CDCL, le CDCL sans saut arrière et le CDCL à ordre partiel. Si le premier supprime totalement la notion de saut arrière en permettant la propagation des clauses unitaires à des niveaux de décision quelconques, le second rend le saut arrière plus sélectif, en désinstanciant uniquement les niveaux de décision qui dépendent du niveau de retour du saut arrière. Notre analyse est à la fois théorique, notamment par une analyse détaillée des propriétés de différentes variations des CDCL sans saut arrière et à ordre partiel, et pratique, puisque l'efficacité de nos contributions est évaluée en les implémentant comme modifications de solveurs SAT de l'état de l'art et en se servant de ces implémentations sur des instances SAT difficiles utilisées lors de compétitions internationales de solveurs. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : problème SAT, satisfaisabilité, formules propositionnelles, CDCL, décomposition arborescente, retour arrière, ordre partiel.

Type: Thèse ou essai doctoral accepté ()
Informations complémentaires: La thèse a été numérisée telle que transmise par l'auteur
Directeur de thèse: Villemaire, Roger
Mots-clés ou Sujets: Algorithme CDCL, Problème SAT
Unité d'appartenance: Faculté des sciences > Département d'informatique
Déposé par: Service des bibliothèques
Date de dépôt: 14 mai 2014 18:20
Dernière modification: 01 nov. 2014 02:27
Adresse URL : http://archipel.uqam.ca/id/eprint/5863

Statistiques

Voir les statistiques sur cinq ans...