 | Recherche DEA |
 |
 |
 |
 |
 |
 |
 |
Sommaire
Sujet
J'ai effectué mon stage de DEA au CRID (Centre de Recherche en Informatique de Dijon) en 1994 sous la direction de Jacqueline Chabrier. Mon sujet portait sur l'utilisation de techniques de symétrie pour la résolution de problèmes SAT :mots clés : Calcul Propositionnel, Problème SAT, Problèmes de Satisfaction de Contraintes (CSP).
Publications
- Resolution of Structured SAT Problems with SCORE(FD/B),
Proceedings of CP'96, Workshop on Constraint Programming Applications, August 19, 1996, Cambridge, Massachusetts, USA
Résumé
Le problème de satisfiabilité d'un ensemble de formules du calcul propositionel (SAT) est un problème fondamental en logique mathématique, inférence, raisonnement automatique. Le problème SAT est NP-complet, i.e. qu'il n'existe pas d'algorithme déterministe de complexité polynomiale capable de résoudre ce problème de manière efficace. En conséquence, de nombreux paradigmes et techniques de programmation ont été développés afin d'améliorer la résolution de ce problème. Citons brièvement les méthodes de saturation (SL-Résolution), les algorithmes énumératifs (Quine, Davis et Putnam), la programmation linéaire en 0-1 (FAST), les méthodes basées sur la recherche locale (Recuit Simulé, Tabu), l'approche programmation par contraintes (CSP, CLP).La méthode SCORE développée au laboratoire CRID s'inscrit dans le cadre de la Programmation par Contraintes. SCORE est une méthode complète et originale de résolution de problèmes de satisfaction de contraintes sur les domaines booléens et entiers offrant un langage déclaratif et statique de haut niveau pour la modélisation des problèmes.
Il est possible de réaliser une classification des problèmes SAT en problèmes structurés et aléatoires. Concernant les problèmes SAT aléatoires, il n'existe a priori pas d'heuristique à caractère général capable de les résoudre tous en apportant un gain de performance majeur.
Par contre, pour les problèmes structurés (tels Ramsey, Pigeons, Schur) la prise en compte des symétries inhérentes à ce type de problèmes donne des résultats intéressants et permet dans certains cas de diminuer de manière drastique le temps de résolution comme en témoignent les résultats que nous avons obtenus.
Dans le cadre de SCORE, le langage de déclaration de problème nous permet de rechercher des symétrie sur l'expression du problèmes, alors que la plupart des méthodes basées sur les symétries recherchent celles-ci lors de la résolution du problème.
Résultats
Le problème des pigeons
Ce problème consiste à déterminer s'il est possible de placer n pigeons dans m pigeonniers, un pigeonnier ne pouvant être occupé au plus que par un seul pigeon.
Pour modéliser ce problème, on utilise n x m variables propositionnelles pi,j avec i variant de 1 à n, et j variant de 1 à m. Si pi,j est vraie alors le pigeon i trouve dans le pigeonnier j.
Ce problème, archétype des problèmes combinatoires, est intéressant sa solution est évidente mais le résoudre peut demander un important temps de calcul :
- si n <= m, le problème est consistant et la recherche d'une solution se fait de manière linéaire sachant que le nombre de solutions (Cmn) est exponentiel,
- si n > m, le problème est inconsistant mais les algorithmes standard (du type Davis et Putnam) prouvent l'inconsistance en un temps exponentiel.
Le problème, écrit en fonction des clauses de cardinalité, s'exprime par :
- chaque pigeon occupe un seul pigeonnier :
#(1,1, p1,1, ..., p1,m) ... #(1,1, pn,1, ..., pn,m)
- chaque pigeonnier contient au plus un pigeon :
#(0,1, p1,1, ..., pn,1) ... #(0,1, p1,m, ..., pn,m)
| Problème | SAT | Variables | Op. Card. | Temps |
 | ||||
| pigeons 11,10 | Non | 110 | 21 | 1 s |
| pigeons 30,29 | Non | 870 | 59 | 55 s |
| ramsey 16 | Oui | 360 | 1800 | 1 s |
| ramsey 17 | Non | 408 | 2176 | 1 s |