Amélioration de l'apprentissage des clauses par symétrie dans les solveurs SAT - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

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.
Fichier principal
Vignette du fichier
benhamou1.pdf (183.35 Ko) Télécharger le fichier
Origine : Accord explicite pour ce dépôt
Loading...

Dates et versions

inria-00519148 , version 1 (18-09-2010)

Identifiants

  • HAL Id : inria-00519148 , version 1

Citer

Belaïd Benhamou, Tarek Nabhani, Richard Ostrowski, Mohamed Réda 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. ⟨inria-00519148⟩
78 Consultations
119 Téléchargements

Partager

Gmail Facebook X LinkedIn More