Exploitation des symétries dans les formules booléennes quantifiées

Résumé : De nombreuses tâches et problèmes combinatoires exhibent des symétries. La résolution de tels problèmes conduit à répéter inlassablement l'étude de situations ou de sousproblèmes équivalents. Depuis plusieurs années, l'exploitation des symétries a permis une réduction significative de l'espace de recherche et la résolution de problèmes ouverts jusqu'alors. Ce paradigme important a été étudié de manière extensive dans de nombreux domaines, comme les problèmes de satisfaction de contraintes (CSP) ou la satisfiabilité de formules booléennes (SAT). L'approche consistant à rajouter des contraintes (symmetry breaking predicates en anglais) est l'une des techniques les plus utilisées pour casser les symétries. Après avoir montré pourquoi il est difficile d'étendre cette approche aux formules booléennes quantifiées, nous montrons comment générer une nouvelle formule équivalente à la formule de départ, mais ne contenant pas de symétries. L'évaluation expérimentale menée sur un des meilleurs solveurs QBF actuels montre des résultats très convaincants sur une grande variété d'instances QBF structurées.
Type de document :
Communication dans un congrès
Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC06), 2006, Nîmes - Ecole des Mines d'Alès / France, 2006
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00085795
Contributeur : Laurent Henocque <>
Soumis le : vendredi 14 juillet 2006 - 11:31:05
Dernière modification le : jeudi 11 janvier 2018 - 06:19:28
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:09:10

Fichier

Identifiants

  • HAL Id : inria-00085795, version 1

Collections

Citation

Gilles Audemard, Said Jabbour, Lakhdar Saïs. Exploitation des symétries dans les formules booléennes quantifiées. Deuxièmes Journées Francophones de Programmation par Contraintes (JFPC06), 2006, Nîmes - Ecole des Mines d'Alès / France, 2006. 〈inria-00085795〉

Partager

Métriques

Consultations de la notice

115

Téléchargements de fichiers

44