La résolution du problème de satisfiabilité
Institution:
MulhouseDisciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
A titre de motivation, nous donnons, dans le chapitre un, une famille d'instances difficiles pour le populaire problème du voyageur de commerce. Les deux chapitres suivants rappellent alors la théorie sous-jacente (classes P et NP, problèmes NP- complets) et se terminent sur le caractère NP-complet pour le voyageur de commerce. L'étude de la résolution débute au chapitre quatre par l'introduction des trames et évaluations, outils qui redonnent d'importants résultats et s'avèrent très utiles par la suite. Au chapitre cinq, nous étudions en toute géneralité la complexité de la résolution sur les formules de Tseitin (définies par des graphes). Notre méthode consiste à interpréter la génération des clauses intermédiaires par des opérations sur le graphe. Pour la mettre en oeuvre, nous devons nous placer dans le cadre des multigraphes quelconques et introduire la notion de cohésion cyclomatique. La complexité de la résolution sur ces formules est alors minorée exponentiellement par cette cohésion. Ce résultat est plus général que celui de A. Urquhart et permet non seulement une minoration mais aussi un calcul de la complexité. Au chapitre six, nous donnons un algorithme de méta-résolution en temps linéaire pour les formules de Tseitin. Cet algorithme repose paradoxalement sur les propriétés qui ont permis de prouver leur caractère intraitable par la résolution