Cooperation control in Parallel SAT Solving: a Multi-armed Bandit Approach

Nadjib Lazaar 1, 2, * Youssef Hamadi 1, 3, 4 Said Jabbour 5 Michèle Sebag 6
* Auteur correspondant
2 TAO - Machine Learning and Optimisation
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Ces dernières années, les solveurs SAT exploite de plus en plus les architectures parallèles, dites de portfolio. Dans ce cadre, un ensemble de procédures CDCL (pour Conflict-Directed Clause Learning en anglais) sont en concurrence et en coopération à travers un partage de clause. Cependant, lorsque le nombre de core augmente (unité de traitement), le partage systématique des clauses apprises durant le procédé CDCL peut ralentir les performances du solveur parallèle. Les précédents travaux ont montré que l'efficacité de l'approche de partage de clause peut être améliorée avec un contrôle dynamique du nombre de clause partagé par les cores [Hamadi et al., IJCAI09], en particulier la taille maximale des clauses autorisée. Dans cet article, une nouvelle approche est proposée pour contrôler la topologie de coopération (paires d'unités autorisées à l'échange de clauses). Cette approche, appelée Ensemble de Bandit pour une résolution SAT Parallèle (BESS, Bandit Ensemble for parallel SAT Solving en anglais). L'approche de coopération BESS s'appuie sur une formalisation de Bandit manchot. BESS est validée empiriquement sur la récente compétition SAT 2012.
Type de document :
Rapport
[Research Report] RR-8070, INRIA. 2012, pp.18
Liste complète des métadonnées

https://hal.inria.fr/hal-00733282
Contributeur : Nadjib Lazaar <>
Soumis le : lundi 17 décembre 2012 - 17:54:04
Dernière modification le : dimanche 16 décembre 2018 - 10:42:01
Document(s) archivé(s) le : dimanche 18 décembre 2016 - 04:14:23

Fichiers

RR-8070.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00733282, version 2

Collections

Citation

Nadjib Lazaar, Youssef Hamadi, Said Jabbour, Michèle Sebag. Cooperation control in Parallel SAT Solving: a Multi-armed Bandit Approach. [Research Report] RR-8070, INRIA. 2012, pp.18. 〈hal-00733282v2〉

Partager

Métriques

Consultations de la notice

849

Téléchargements de fichiers

369