Encadrement : Lakhdar Saïs et Gilles Audemard

Laboratoire : Centre de Recherche en Informatique de Lens

E-mail : sais@cril.univ-artois.fr audemard@cril.univ-artois.fr

Web : http://www.cril.univ-artois.fr/~sais http://www.cril.univ-artois.fr/~audemard

 
Contexte et objectifs scientifiques :

Les symétries font parties de notre quotidien. Elles apparaissent dans de nombreux problèmes de la vie courante, et sont utilisés largement dans des domaines variés comme la physique, la chimie ou encore les mathématiques. Pourtant, les stratégies visant à supprimer ces isomorphismes ont fait leur apparition il y a moins de 20 ans. L’exploitation des symétries pour réduire la complexité des problèmes est devenue un thème important dans le cadre des problèmes de satisfaction de contraintes (CSP), de la résolution de formules booléenne (SAT), et plus récemment dans le cadre de ses extensions : les formules booléennes quantifiées (QBF) et les contraintes pseudo booléennes (CPB). L’étude des symétries couvre donc un champ d’application de plus en plus élargie. Dans tous les cas, deux problèmes sont généralement étudiés : la détection des symétries et leurs exploitations.

Détection : D’un point de vue théorique, la détection des symétries est équivalente au problème de décision de l’isomorphisme de deux graphes. Ce problème pour lequel on ne connaît pas d’algorithme polynomial reste ouvert. D’un point de vue pratique, il existe des algorithmes permettant de la détection des symétries (e.g. NAUTY). Le meilleur algorithme est issu des travaux sur le problème de l’isomorphisme de graphe. On peut tout de même distinguer deux approches : celles qui supposent que les symétries sont données à priori (dans les spécifications du problème lui-même) et celles qui effectuent une reconnaissance automatique des symétries du problème. Cette étape de détection est généralement effectuée sur la formule originale.

Exploitation : Les symétries permettent de partitionner l’ensemble des configurations en classes d’équivalences. Chaque classe contient les configurations symétriques. L’objectif est de réduire l’exploration de l’espace des configurations a une configuration par classe d’équivalences. L’élimination des configurations isomorphes est généralement réalisée en ajoutant des contraintes supplémentaires à la formulation du problème. Cet ensemble de contraintes additionnelles peut généralement s’avérer de taille exponentielle dans le pire cas.

Malgré les inconvénients cités ci-dessus, l’exploitation des symétries reste une approche viable en pratique. En effet sur de nombreux problèmes issus d’applications réels, les gains obtenus dépassent largement le coût de la détection et de l’exploitation.

Le but de ce stage est dans un premier temps de faire un bilan des approches proposées en effectuant une synthèse et une classification des différentes techniques. Dans un second temps pointer les différences entre les approches utilisées dans le cadre de SAT ,CSP et QBF.

Les objectifs de ce stage de Master 2 (qui peut être poursuivi en thèse) sont multiples, il s’agit d’étudier les différentes pistes énumérées ci-dessous :

1. Détection et exploitation dynamique : Alors que la majorité des travaux détecte et élimine les symétries en phase de pré-traitement, il s’agit d’étudier la faisabilité de l’approche dynamique (détection et exploitation en cours de recherche). Cette approche a été initiée par Benhamou et Saïs au début des années 90. Revisiter cette approche et proposer des améliorations nous paraît très important. Il s’agit en particulier de l’évaluer sur les nouvelles bases de tests actuellement disponibles. L’avantage de cette approche est que des symétries nouvelles peuvent apparaître au cours de la résolution. Cette approche est à relier avec l’exploitation des symétries locales alors que les approches traditionnelles n’exploitent que les symétries globales du problème.
2. Etudier de nouvelles formes de symétries comme par exemple les symétries forte introduite par Benhamou et Saïs en 1994 et de nouvelles formes de symétries beaucoup plus puissantes comme les symétries locales ou encore les homomorphismes définis récemment par Stefan Szeider de l'université de Toronto.

Bibliographie :

[1] Belaïd Benhamou, Lakhdar Saïs, Tractability Through Symmetries in Propositional calculus, Journal of Automated Reasoning, 12 :89-102,1994.

[2] Belaïd Benhamou, Pierre Siegel et lakhdar Saïs, Dealing with cardinality in propositional calculus, Workshop on tractable reasoning, AAAI92

[3] Gilles Audemard, Lahdar Saïs, Dealing with symmetries in Quantified Boolean Formulas, Proceedings of International Conference en Satisfiaility Testing SAT’2004, Vancouver 2004.

[4] Stephan Szeider, The Complexity of Resolution with Generalized Symmetry Rules; Proceedings, STACS 2003, Eds.: H. Alt, M. Habib; Lecture Notes in Computer Science 2607, pp. 475-486, Springer Verlag 2003.

[5] Stephan Szeider, Generalizations of Matched CNF Formulas; to appear in Annals of Mathematics and Artificial Intelligence.

[6] Stephan Szeider, Homomorphisms of Conjunctive Normal Forms; Discrete Applied Mathematics vol. 130 no. 2, pp. 351-365, 2003.