Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/inria-00519148
Contributor : Christophe Lecoutre <>
Submitted on : Saturday, September 18, 2010 - 3:20:23 PM
Last modification on : Monday, March 30, 2020 - 8:44:54 AM
Long-term archiving on: : Sunday, December 19, 2010 - 2:43:01 AM

File

benhamou1.pdf
Explicit agreement for this submission

Identifiers

  • HAL Id : inria-00519148, version 1

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. ⟨inria-00519148⟩

Share

Metrics

Record views

158

Files downloads

182