SAT en Parallèle

De nos jours, les ordinateurs sont de plus en plus exploités afin de résoudre de nombreux problèmes réels émanant de différents domaines. Destiné à cette tâche, le problème SAT (pour problème de SATisfaisabilité booléenne) s’appuie sur une modélisation en logique propositionnel des applications pour les résoudre. L’une des raisons du succès de SAT est la mise à disposition pour l’utilisateur de solveurs efficaces. En effet, les résultats de ces derniers sont très impressionnants et permettent la modélisation d’un grand nombre de problèmes réels (pouvant contenir des millions de variables et de clauses). Parmi les problèmes qui ont fait le succès de SAT, nous pouvons citer la vérification de modèles bornés (Biere et al. 1999), la planification (Kautz et Selman 1996), la résolution de problèmes combinatoires tel que les quasigroupes (Bennett et Zhang 2004a) et les nombres de Ramsey et Van der Waerden (Herwig et al. 2007). Plus récemment, l’utilisation du paradigme SAT a permis de résoudre la conjecture des triplets pythagoriciens (Heule et al. 2016). En plus, le problème SAT est pilier de la théorie de la complexité. En effet, c’est le premier problème a avoir été prouvé NP-complet (Cook 1971). De ce fait, de nombreux autres problèmes (extraction de MUS (Marques-Silva et Lynce 2011), logique modale (Lagniez et al. 2017), . . . ) sont souvent résolus au moyen d’une réduction vers SAT plutôt qu’avec des démonstrateurs ad-hoc.

Longtemps étudié dans un contexte séquentiel, le problème SAT a fait éclore des algorithmes efficaces et puissants. Ceci s’explique à la fois par l’amélioration des solveurs SAT basés sur l’algorithme CDCL (apprentissage, VSIDS, watched literal,…) et l’accroissement de la fréquence des processeurs.  une amélioration constante des solveurs SAT séquentiels au cours de ces deux dernières décennies. Cela est dû, notamment, à l’émulation apportée par les nombreuses applications et compétitions liées à SAT. Ainsi, grâce à cette émulation, chaque année de nombreuses améliorations sont apportées aux solveurs SAT. Ainsi, en 2017, la technique inprocessing appelée Learnt Clause Minimization s’est vue être particulièrement efficace (Luo et al. 2017).

La parallélisation des algorithmes de résolution pour SAT constitue un autre axe d’amélioration. Ceci est renforcé par le fait qu’à l’heure actuelle la puissance de calcul d’un ordinateur ne se traduit plus par une augmentation des fréquences du microprocesseur, mais par l’augmentation du nombre de cœurs de calcul au sein de celui-ci. Par conséquent, afin d’utiliser tout le potentiel des ordinateurs, le parallélisme d’un solveur SAT est aujourd’hui une obligation. Qui plus est, grâce à l’essor du cloud computing, il est désormais possible de solliciter un nombre conséquent de machines virtuelles pouvant être disponibles en quelques secondes.

Dans la résolution parallèle du problème SAT, les solveurs peuvent être divisés en deux catégories. Premièrement, les solveurs de type portfolio lancent, sur la formule originale, différentes heuristiques/stratégies en concurrence (Audemard et al. 2012, Balyo et al. 2015, Biere 2014, Hamadi et al. 2009a;c, Roussel 2011). Pendant la résolution, les processus échangent des informations (généralement sous la forme de clauses apprises) afin de s’entraider (Audemard et al. 2012, Audemard et Simon 2014, Hamadi et al. 2009a;c). Deuxièmement, les solveurs basés sur le paradigme « diviser pour mieux régner » découpent l’espace de recherche en plusieurs sous espaces afin de les distribuer à des solveurs SAT, communément nommés workers. En général, à chaque fois qu’un solveur a fini de résoudre son sous-problème (tandis que les autres travaillent encore), une stratégie d’équilibrage est appliquée afin de transférer dynamiquement un nouveau sous-espace à ce worker inactif (Chrabakh et Wolski 2007, Chu et al. 2008). Les sous-espaces peuvent être définis en utilisant le concept du chemin de guidage (guiding path (Zhang et al. 1996)), généré statiquement (avant la recherche (Heule et al. 2012, Semenov et Zaikin 2015)), ou dynamiquement (pendant la recherche (Audemard et al. 2014b, Hyvärinen et al. 2010a, van der Tak et al. 2014)). Comme dans les solveurs de type portfolio, les clauses apprises peuvent aussi être partagées (Feldman et al. 2005).

Malheureusement, l’adaptation des algorithmes SAT vers le parallélisme se complexifie avec ses nombreuses améliorations séquentielles, mais aussi, à cause des nouvelles architectures mises en place par les constructeurs. Plus précisément, un nouveau type d’architecture appelé many-cores demande aux programmeurs de changer leurs manières de coder. Cela est déjà arrivé dans le passé puisque un programmeur en parallélisme doit aujourd’hui posséder des notions à la fois liées au multi-cores et au passage de messages entre plusieurs machines (socket, MPI, . . .). En plus de cela, les solveurs SAT parallèles ne passent pas à l’échelle. Précisément, les gains dûs au parallélisme des solveurs SAT s’amenuisent à partir d’un certain nombre d’unités de calcul. Notamment, lors de la SAT compétition 2017, le gagnant du Parallel Track a choisi d’utiliser seulement la moitié des cœurs d’une machine, c’est-à-dire, 24 des 48 cœurs disponibles. Même si cette compétition utilisait 48 cœurs de calcul, 24 d’entre eux étaient hyper-threaded. En pratique, grâce aux résultats de cette compétition, nous pouvons nous apercevoir que l’hyper-threading n’est pas toujours efficace avec les solveurs SAT parallèles.

Le principale désavantage dans le multi-cores est son nombre limité d’unité de calcul. Pourtant, une manière pour un solveur SAT d’exploiter le potentiel du parallélisme est l’utilisation de plusieurs ordinateurs. Alors qu’une seule machine à un nombre limité d’unités de calcul, les clusters de calcul peuvent en apporter beaucoup plus et s’étendre en théorie à l’infini. Néanmoins, un solveur mutli-thread utilisant uniquement une librairies gérant la mémoire partagée ne peut pas exploiter correctement des techniques propres à SAT (partages des clauses, décomposition du problème, . . . ) sur plusieurs machines. Afin de pallier ce problème, il est alors nécessaire de basculer vers les architectures distribuées. Le but principal de cette thèse est d’améliorer SAT en distribué. Nos contributions s’articulent donc autour des deux approches de résolution parallèle du problèmes SAT ( portfolio et « diviser pour mieux régner ») dans un cadre massivement distribué.

Une machine de Turing est un modèle mathématique de calcul définissant une machine abstraite (basée sur un modèle théorique) qui manipule un ensemble fini de symboles en changeant le contenu des cases d’un tableau infini selon des règles.

Définition 1.18 (Problème NP-complet). Dans la théorie de la complexité, un problème NP-complet est un problème de décision appartenant à la fois à la classe NP et à la classe NP-difficile. Dans ce contexte, NP signifie « Non-déterministe Polynomial » car il peut être résolu par une machine de Turing non-déterministe en un temps polynomial. Un problème est NP-difficile si il est au moins aussi difficile que tous les autres problèmes de la classe NP.

Bien que toute solution donnée à un problème NP-complet peut être vérifié rapidement (en temps polynomial), il n’y a pas de moyen efficace connu pour trouver une solution. Autrement dit, le temps nécessaire pour résoudre le problème en utilisant des algorithmes connus augmente très rapidement (exponentiellement) en fonction de la taille du problème. Les problèmes appartenant au complémentaire de NP sont dit coNP. Le problème complémentaire de la satisfaisabilité (il existe une interprétation qui satisfait la formule) d’une formule est le problème vérifiant sa validité (toutes les interprétations satisfont la formule, ce qui est équivalent, il n’existe pas d’interprétation qui satisfait la négation de la formule).

La structure des formules propositionnelles a un impact colossal sur leur résolution. D’un coté, la satisfaisabilité d’une formule DNF peut être vérifiée en un temps linéaire : il suffit de vérifier si au moins une de ces conjonctions est satisfaisable. Une telle conjonction est satisfaisable si elle ne contient pas à la fois un littéral et son complémentaire. Plus encore, une formule DNF exprime directement tous ses modèles par sa structure. Cependant, vérifier la validité d’une formule DNF est difficile (coNPcomplet).

À contrario, dans le cas d’une formule CNF, vérifier la satisfaisabilité est difficile (NP-complet) tandis que vérifier sa validité est facile (il suffit d’examiner chaque clause de la CNF). En d’autres mots, même si résoudre la satisfaisabilité d’une formule DNF est trivial, celle d’une formule CNF est amplement plus difficile (NP-complet). En effet, pour traduire une formule CNF en DNF, un nombre exponentiel de termes peut être construit au cours de la traduction, de sorte que la traduction elle-même ne peut pas s’exécuter en un temps polynomial. Clairement, une telle traduction consiste à résoudre la formule afin de trouver tous ses modèles.

Le rapport de stage ou le pfe est un document d’analyse, de synthèse et d’évaluation de votre apprentissage, c’est pour cela rapport-gratuit.com propose le téléchargement des modèles complet de projet de fin d’étude, rapport de stage, mémoire, pfe, thèse, pour connaître la méthodologie à avoir et savoir comment construire les parties d’un projet de fin d’étude.

Table des matières

Introduction générale
État de l’art
Chapitre 1 Le problème SAT
1.1 Logique propositionnelle
1.1.1 Syntaxe
1.1.2 Sémantique
1.1.3 Formes normales
1.2 Théorie de la complexité
1.3 Problème SAT
1.3.1 Encodages
1.3.2 Fragments polynomiaux
1.4 Applications
1.4.1 Exemples
1.5 Conclusion
Chapitre 2 Résolution séquentielle du problème SAT
2.1 Approches complètes ou incomplètes
2.1.1 Approches incomplètes
2.1.2 Approches complètes
2.1.3 Comparaison
2.2 Genèse des solveurs SAT
2.2.1 Résolution
2.2.2 L’algorithme Davis – Putnam
2.2.3 L’algorithme de Davis – Logemann – Loveland
2.3 Les solveurs SAT
2.3.1 Apprentissage
2.3.2 L’algorithme CDCL
2.3.3 Choix de variable et choix de polarité
2.3.4 Structure de données paresseuses
2.3.5 Politiques de suppression des clauses apprises
2.3.6 Stratégies de redémarrage
2.3.7 Prétraitement
2.3.8 Inprocessing
2.4 Conclusion
Conclusion générale

Rapport PFE, mémoire et thèse PDFTélécharger le rapport complet

Télécharger aussi :

Laisser un commentaire

Votre adresse e-mail ne sera pas publiée. Les champs obligatoires sont indiqués avec *