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
CNRS - Centre National de la Recherche Scientifique : UMR8623, Inria Saclay - Ile de France, UP11 - Université Paris-Sud - Paris 11, LRI - Laboratoire de Recherche en Informatique
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 : jeudi 11 janvier 2018 - 06:22:37
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

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

738

Téléchargements de fichiers

305