Amélioration de l'apprentissage des clauses par symétrie dans les solveurs SAT

Résumé : Le problème de satisfiabilité (SAT) est le premier problème de décision à avoir été montré NP-complet. Il est central en théorie de la complexité. Une for- mule mise sous forme CNF contient un nombre inté- ressant de symétries. En d'autres termes, la formule reste invariante si l'on permute quelques variables. De telles permutations sont les symétries de la formule et leurs éliminations peuvent conduire à une preuve plus courte pour la satisfiabilité. D'autre part, de nom- breuses améliorations ont été apportées dans les sol- veurs actuels. Les solveurs de type CDCL sont aujour- d'hui capables de résoudre de manière efficace des problèmes industriels de très grande taille (en nombre de variables et de clauses). Ces derniers utilisent des structures de données paresseuses, des politiques de redémarrage et apprennent de nouvelles clauses à chaque échec au cours de la recherche. Bien que l'uti- lisation des symétries et l'apprentissage de clauses s'avèrent être des principes puissants, la combinai- son des deux n'a encore jamais été exploitée. Dans cet article, nous allons montrer comment la symétrie peut être utilisée afin d'améliorer l'apprentissage dans des solveurs de type CDCL. Nous avons mis en ap- plication l'apprentissage par symétries dans MiniSat et nous l'avons expérimenté sur différents problèmes. Nous avons comparé MiniSat avec et sans apprentis- sage par symétries. Les résultats obtenus sont très en- courageants et montrent que l'utilisation des symétries dans l'apprentissage est profitable pour des solveurs à base de CDCL.
Type de document :
Communication dans un congrès
JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.71-80, 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00519148
Contributeur : Christophe Lecoutre <>
Soumis le : samedi 18 septembre 2010 - 15:20:23
Dernière modification le : jeudi 18 janvier 2018 - 02:20:51
Document(s) archivé(s) le : dimanche 19 décembre 2010 - 02:43:01

Fichier

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

Identifiants

  • HAL Id : inria-00519148, version 1

Collections

Citation

Belaïd Benhamou, Tarek Nabhani, Richard Ostrowski, Mohamed Saïdi. Amélioration de l'apprentissage des clauses par symétrie dans les solveurs SAT. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.71-80, 2010. 〈inria-00519148〉

Partager

Métriques

Consultations de la notice

96

Téléchargements de fichiers

125