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 :

Symétries dans les Problèmes SAT structurés, Application à Score(FD/B)

mots clés : Calcul Propositionnel, Problème SAT, Problèmes de Satisfaction de Contraintes (CSP).

Publications


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.

Spécification des problèmes

Le probème de coloriage de Ramsey

proc Ramsey(N) {
	int I,J,K;
	array red[N][N], green [N][N], blue [N][N];

	/* One edge has one and only one color */
	foreach I in 1..N-1
		foreach J in I+1..N
			#(1,1, red[I][J], green[I][J], blue[I][J] );

	/* There is no monochromatic triangle */
	foreach I in 1..N-2
		foreach J in I+1..N-1
			foreach K in J+1..N
			{
				#(0,2, red[I][J], red[I][K], red[J][K] );
				#(0,2, green[I][J], green[I][K], green[J][K] );
				#(0,2, blue[I][J], blue[I][K], blue[J][K] );
			}
}
proc PigeonHole(N, P) {
	int I;
	array pig[N][P];
	
	/* One pigeon is in one and only one dovecote */
	foreach I in 1..N
		#(1, 1, pig[I][*]);

	/* In a dovecote, there is 1 pigeon maximum */
	foreach I in 1..P
		#(0, 1, pig[*][I]);
}

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 :

Le problème, écrit en fonction des clauses de cardinalité, s'exprime par :

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
Résultats obtenus par Score(FD/B) - 1996