Résolution parallèle de SAT: mieux collaborer pour aller plus loin

Résumé : La gestion de la base de clauses apprises est connue pour être une tâche ardue au sein des solveurs SAT. Dans le cadre des solveurs parallèles de type portfolio, la collaboration réalisée entre les différents processus au moyen de l'échange de clauses rend cette gestion plus complexe encore. Différentes techniques ont été proposées ces dernières années, mais les résultats pratiques restent en faveur de solveurs ayant une collaboration limitée voire nulle. Ceci est principalement dû au fait que chacun des processus doit gérer le grand nombre de clauses générées par les autres. Dans cet article, nous proposons une nouvelle technique efficace pour l'échange de clauses au sein d'un solveur parallèle. Contrairement aux méthodes actuelles, notre approche repose sur des politiques pour l'exportation et pour l'importation de clauses, tout en utilisant des techniques récentes, qui ont prouvées leur efficacité dans le cadre séquentiel. Un grand nombre d'expérimentations tend à montrer l'intérêt des idées proposées.
Type de document :
Communication dans un congrès
JFPC 2012, 2012, Toulouse, France. 2012
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00818239
Contributeur : Benoît Hoessen <>
Soumis le : vendredi 26 avril 2013 - 14:46:55
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : mardi 4 avril 2017 - 00:00:55

Fichier

paper_6.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00818239, version 1

Collections

Citation

Gilles Audemard, Benoît Hoessen, Said Jabbour, Jean-Marie Lagniez, Cédric Piette. Résolution parallèle de SAT: mieux collaborer pour aller plus loin. JFPC 2012, 2012, Toulouse, France. 2012. 〈hal-00818239〉

Partager

Métriques

Consultations de la notice

188

Téléchargements de fichiers

64