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.

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 :

Voici la représentation du problème en SCORE(FD/B) :

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]);
}

Le problème de coloriage de Ramsey

Le problème de Ramsey, ici en trois couleurs (rouge, vert, bleu), consiste à colorier les triangles d'un graphe complet sans qu'il n'y ait de triangle monochromatique (une seule couleur).

Ce problème admet des solutions pour $3 ≤ n ≤ 16$ et n'admet pas de solution au dela de 16.

Voici la représentation du problème en SCORE(FD/B) :

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] );
			}
}

Temps de résolution

Nous présentons ci-dessous les résultats obtenus à l'époque sur une Station SUN Sparc 10.

Le symbole Inf indique que le programme a été arrêté après deux jours de calculs.

 Problème   Sat   Vars   Ctrs   Temps   Temps + Sym 
 Pigeon 10, 10   Oui   100   20   1   1 
 Pigeon 10, 9   Non   90   19   45   1 
 Pigeon 30, 30   Oui   900   60   1   1 
 Pigeon 20, 29   Non   870   59   Inf   55 
 Ramsey 14   Oui   273   1183   1   1 
 Ramsey 15   Oui   315   1470   48   1 
 Ramsey 16   Oui   360   1800   3m45   1 
 Ramsey 17   Non   408   2176   Inf   1 
RĂ©sultats obtenus par Score(FD/B) - 1996