Langages concurrents avec contraintes basés sur la logique linéaire.
François Fages, INRIA, Rocquencourt.

On peut donner une sémantique logique des langages concurrents avec contraintes (CC) dans la logique linéaire de Jean-Yves Girard, permettant de caractériser les succés ainsi que les stores accessibles des calculs CC. Cette sémantique suggère de généraliser les systèmes de contraintes classiques en considérant des systèmes de contraintes basés sur la logique linéaire. Nous montrons comment cette extension permet de généraliser l'approche "boite de verre" de CC à la reconstruction de solveurs de contraintes globales.

Application des Contraintes à l'Extraction de Connaissances dans les Bases de Données
Christel Vrain, LIFO, Orléans.

L'Extraction de Connaissances dans les Bases de Données (ECD) est un domaine de recherches qui connaît un essor considérable, ces dernières années, étant données ses applications industrielles et commerciales potentielles. Le processus d'ECD se décompose en plusieurs étapes : récupération des données, pré-traitement, fouille de données et enfin validation. Dans cet exposé, nous nous intéressons au formalisme des contraintes pour modéliser plusieurs tâches inhérentes au processus de fouille de données, principalement lorsque celui-ci repose sur des mécanismes d'apprentissage inductif et lorsqu'il est vu comme la recherche d'une ``bonne'' hypothèse, à l'intérieur d'un espace de recherches. - La Programmation Logique avec Contraintes nous donne un formalisme pour modéliser l'apprentissage inductif dans le cas de données numériques et symboliques. L'espace de recherche est alors constitué de clauses contraintes, respectant des critères syntaxiques prédéfinis par l'utilisateur et que l'on appelle des biais d'apprentissage. Les Bases de Données Contraintes nous offrent de plus un moyen de représenter et de stocker des informations infinies. Elles sont particulièrement bien adaptées à la représentation des données spatiales. - Les biais d'apprentissage peuvent être modélisées par des grammaires d'arbres avec contraintes, ce qui permet d'élaguer l'espace de recherches lors de la génération d'hypothèses satisfaisant ces biais. Les opérateurs de spécialisation sont aussi modélisées dans ce formalisme. Nous conclurons cet exposé par une présentation d'une application de l'ECD aux bases de données géographiques, application développée actuellement dans le cadre d'une collaboration avec le BRGM.

Un outil pour résoudre les problèmes NP-complets sur une architecture reconfigurable.
SAT-reduction: a tool to solve NP-complete probleme on reconfigurable architectures.

Zineb Habbas (GIFM, Metz), Francine Herrmann (GIFM), Michael Krajecki (LERI, Reims) and Daniel Singer (GIFM).

Due to recent advances in FPGA (Field Programmable Gate Arrays) and High-Level Logic Synthesis the feasibilty to create a logic circuit dedicated to solve one SAT problem instance has been proved. Some propositions investigate incomplete local search algoritms such as GSAT or complete enumerative ones such as DPLL (Davis-Putnam-Logemann-Loveland). Here we remain the good old polynomial SAT-reductions as the first tile to build FPGA-based resolution of any NP-Complete problem. The two relevant points of this approach are: efficient encodings of the NP-Complete problem into SAT and efficient heuristics to solve them in the SAT formalism.
Two theoretical results encourage this new direction. A lot of NP-complete problems are easy (constant or polynomial time) on average for some distribution, moreover hard instances are infrequent. This makes the instance-based resolution methodology specially adapted. The second one is that for the k-SAT model (clauses length fixed to k) there is an hard region where the probability to find an hard instance is near 1, defined by some threshold expressed as t= C x number(clauses)/number(variables). This makes the clauses parallelism offered by Hardware implementation well suited in this area.
We give some preliminary results for the well known Graph Colouring Problem wich is a special case of the Constraint Satisfaction Problem on finite domains.

Stratégies parallèles de propagation d'intervalles : résultats et perspectives
Laurent Granvilliers (IRIN, Nantes) et Gaétan Hains (LIFO, Orléans)

La problématique générale des algorithmes parallèles de propagation d'intervalles a été définie lors de la journée LODEC de décembre 1998. Depuis, un nouvel algorithme parallèle de calcul de la box consistency a été étudié, implanté et porté sur deux architectures différentes de machine parallèle. Dans le même temps, de nouveaux algorithmes séquentiels ont été développés. En particulier, citons HC4 effectuant des parcours des représentations arborescentes des contraintes, BC4 combinant HC4 et l'algorithme classique BC3 de calcul de la box consistency, et BC5 combinant HC4, BC3 et Gauss-Seidel sur les intervalles. Ainsi, de nouveaux problèmes apparaissent, en particulier le choix des algorithmes ou morceaux d'algorithmes à paralléliser. Cet exposé présentera succinctement les résultats et perspectives relatifs à ce travail.

Travaux récents en programmation parallèle fonctionnelle
1. Compilation d'un langage fonctionnel spécialisé pour machine parallèle
Julien Mallet, IRISA, Rennes.

Les langages de programmation utilisés pour les machines parallèles sont soit des langages à parallélisme explicite efficaces mais non portables et très complexes à utiliser, soit des langages simples et portables mais leur compilation est complexe et relativement inefficace. Nous proposons un langage spécialisé basé sur des shémas de programme (patrons) encapsulant des flôts de donnée et de contrôle pour lequel une analyse de coût exacte de l'implantation parallèle existe. Le schéma de compilation proposé vise à choisir automatiquement les distributions des données sur les processeurs grâce au coût exact assuré par le langage source. Ceci permet d'obtenir une compilation automatique tout en conservant un code parallèle efficace (les distributions représentant un choix d'implantation parallèle global). Notre schéma de compilation est composé d'une suite de transformations et d'analyses automatiques de programmes. Chaque transformation transforme un langage à patrons dans un autre plus proche d'un code à parallélisme explicite. Le langage cible est un langage à patrons décrivant des programmes SPMD directement traduisible en un langage séquentiel avec des appels à des primitives de bibliothèque de communication. Les étapes principales de compilation sont l'analyse de taille, la transformation de modification en place, l'explicitation des communications et la distribution des données.

2. Conception de langages fonctionnels pour la programmation massivement parallèle
Frédéric Loulergue et Gaétan Hains, LIFO, Orléans

Le schéma d'exécution bulk-synchronous parallelism (BSP) a été proposé par Valiant en 1990 comme modèle réaliste et portable des algorithmes parallèles. Il permet une prévision assez fiable des performances en fonction de la bande passante et de la latence du réseau. Le prix à payer est l'utilisation d'une famille d'algorithmes "plats" c'est-à-dire sans composition parallèle ni emboîtement et dont les synchronisations sont toutes globales.
Dans le but de simplifier la programmation BSP sans sacrifier son aspect quantifiable, nous avons cherché à concevoir un langage purement fonctionnel dans lequel les évaluations sont des calculs BSP et muni d'une composition parallèle assez faible pour être interprétée par des calculs plats. Nous montrons que le permier objectif peut être atteint en proposant une extension confluente du lambda-calcul, une variante vectorielle de celle-ci et une sémantique opérationnelle répartie équivalente, comme modèle d'implantation. Cependant la conception d'une composition parallèle faible est un échec pour cause de non-confluence.

Clôture par congruence modulo associativité et commutativité
Laurent Vigneron, LORIA - Université Nancy 2

L'expression "clôture par congruence" a typiquement été utilisée pour dénoter certaines structures de données représentant les relations de congruence induites par des ensembles d'équations closes. Les clôtures par congruence ont été utilisées pour décider si une égalité $s \simeq t$ est une conséquence logique d'un ensemble d'équations composées de termes construits à partir de constantes et d'opérateurs de fonction non interprétés. Nous définissons une clôture par congruence abstraite et présentons un ensemble de règles de transition permettant de construire une telle clôture. Ce point de vue abstrait a de nombreux avantages: il permet de mieux comprendre les algorithmes existants basés sur la construction de graphes; il a été facilement étendu pour traiter le cas d'opérateurs associatifs et commutatifs; il permet d'obtenir des procédures beaucoup plus efficaces; il permet de construire efficacement un système de réécriture convergent. Ce travail a été réalisé en collaboration avec Leo Bachmair, I. V. Ramakrishnan et Ashish Tiwari, de l'Université de Stony Brook (NY).

Evaluation de spécifications formelles en PLC ensembliste
Laurent Py, LIB, Besançon

I Problématique et contexte.
Nous avons défini une approche fondée sur des techniques de Satisfaction de Contraintes Ensemblistes pour l'évaluation de spécifications formelles logico-ensemblistes B avec comme pricipales cibles applicatives : un animateur contraint et un model-checker contraint.

II Résolution de contraintes ensemblistes.
Nous avons développé un solveur ensembliste spécifique, CLPS-B, utilisant une représentation énumérative des domaines. Ces domaines sont représentés par des ensembles de constantes mais également de variables. Cette représentation est induite par les contraintes engendrées durant l'évaluation de la spécification. Des règles d'inférences spécifiques ont alors été définies pour assurer une propagation efficace dans ce contexte particulier.

III Evaluation contrainte et applications.
Nous avons défini à partir de CLPS-B une méthodologie d'évaluation contrainte. Nous avons notamment expérimenté cette approche pour réaliser une animation contrainte de plusieurs machines B.