Communication

JaCk-SAT : un algorithme de résolution parallèle du problème SAT par décomposition structurelle

Anthony Monnet

Membre a labase

Anthony Monnet

Résumé de la communication

Le problème de la satisfaisabilité d'une formule logique propositionnelle, ou problème SAT, est très étudié en informatique, car nombre de problèmes de décision théoriques ou pratiques peuvent être traduits facilement en un problème SAT équivalent. Bien qu'il soit connu depuis 1971 comme NP-complet, de nombreuses recherches ont été menées avec succès afin d'améliorer l'efficacité de sa résolution en pratique. Parmi les nombreuses thématiques actuellement explorées, se trouvent d'une part l'utilisation d'architectures parallèles, dont le but est de répartir la charge de calcul de la résolution entre plusieurs processeurs, et d'autre part la décomposition des problèmes traités, qui consiste, au lieu de traiter le problème global, à le décomposer en sous-problèmes, puis à retrouver les solutions du problème global à partir de celles des sous-problèmes. Nous présenterons la méthode JaCk-SAT (pour Join and Check, soit jointure et vérification), qui combine ces deux approches, c'est-à-dire qu'elle réalise une décomposition du problème SAT, puis résout les sous-problèmes parallèlement, avant de retrouver les solutions du problème global par une jointure (également en parallèle) des solutions des sous-problèmes. Nous exposerons également nos résultats expérimentaux, obtenus par une implémentation de l'algorithme sur des architectures à mémoire distribuées, et évoquerons quelques pistes pour des travaux futurs.

Contexte

Section :

L'Énoncé de politique des trois Conseils nouvelle version : application au contexte québécois

Domaine de la communication :

L'Énoncé de politique des trois Conseils nouvelle version : application au contexte québécois

Date : 8 mai 2008

Hôte : Institut national de la recherche scientifique

Découvrez d'autres communications scientifiques

Dans le même domaine
Du même congressiste

Thème de la communication :

L'Énoncé de politique des trois Conseils nouvelle version : application au contexte québécois

Monoparentalité et réseaux de soutien. Les parcours de vie des mères immigrées à Québec

Ana Gherghel

Mesure de la floculation d'une suspension fibreuse par réflectométrie laser

Rudolph Ahanda-Mbock

Les effets sur les élèves de l'intégration de la dimension culturelle à l'école : analyse du discou…

Héloïse Côté

Voir tous les contenus de cette communication

Autres communications du même congressiste :

Domaine de la communication :

L'Énoncé de politique des trois Conseils nouvelle version : application au contexte québécois

JaCk-SAT : un algorithme de résolution parallèle du problème SAT par décomposition structurelle

Anthony Monnet