Sommaire

• Sujet
• Publications
• Résumé
• Résultats

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

• Resolution of Structured SAT Problems with SCORE(FD/B),
  Proceedings of CP'96, Workshop on Constraint Programming Applications, August 19, 1996, Cambridge, Massachusetts, USA (pdf)

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 p_i,j avec i variant de 1 à n, et j variant de 1 à m. Si p_i,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 (C_mⁿ) 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)

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.

• la colonne Sat indique si le problème est satisfiable ou non
• la colonne Vars donne le nombre de variables du problème
• la colonne Ctrs donne le nombre de contraintes du problème
• la colonne Temps indique le temps de résolution en minutes et secondes sans symétries
• la colonne Temps + Sym indique le temps de résolution en minutes et secondes avec utilisation de symétries

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