Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00085795
Contributor : Laurent Henocque <>
Submitted on : Friday, July 14, 2006 - 11:31:05 AM
Last modification on : Thursday, January 11, 2018 - 6:19:28 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 12:09:10 AM

File

Identifiers

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

Share

Metrics

Record views

157

Files downloads

78