Combinaison des règles d'inférence et de la sous-estimation des bornes inférieures pour Max-SAT

Résumé : Le calcul de la borne inférieure (LB) pour les solveurs Max-SAT basés sur la méthode de Séparation et Évaluation (Branch and bound) a généralement deux composantes : (i) la composante sous-estimation, qui détecte les sousformules disjointement inconsistantes et considère le nombre de ces sous-formules détectées comme une sous-estimation de LB, et (ii) la composante inférence, qui applique les règles d'inférence qui, dans le meilleur des cas, explicitent une contradiction permettant d'incrémenter LB. Dans ce papier, nous nous concentrons sur l'interaction entre la composante sous-estimation et la règle d'inférence dite résolution de cycle, qui a été récemment montrée très puissante dans deux solveurs Max-SAT de l'état-de-l'art : MAX-DPLL et MaxSatz. MAX-DPLL applique la règle de résolution de cycle de façon exhaustive, mais ne combine pas son application à la composante calculant la sous-estimation, tandis que Max- Satz le fait mais avec une application limitée de la résolution de cycle. Notre objectif est d'obtenir une meilleure intégration de la règle de résolution de cycle avec la composante sous-estimation afin d'améliorer la qualité de LB. Dans ce but, nous avons défini plusieurs heuristiques qui guident l'application de la résolution de cycle dans MaxSatz. La plus performante de ces heuristiques nous a permis d'obtenir une variante de MaxSatz, appeléeMaxSatzc, qui applique la résolution de cycle lorsque la composante sous-estimation est susceptible de détecter des sous-formules inconsistantes. Notre étude expérimentale montre que MaxSatzc améliore substantiellement MaxSatz sur un nombre considérable d'instances difficiles.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.287-295, 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00292665
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : mercredi 2 juillet 2008 - 12:13:30
Dernière modification le : vendredi 11 juillet 2008 - 18:24:30
Document(s) archivé(s) le : vendredi 28 mai 2010 - 23:04:41

Fichier

pages-287-295-article18.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00292665, version 1

Collections

Citation

Chu Min Li, Felip Manya, Nouredine Ould Mohamedou, Jordi Planes. Combinaison des règles d'inférence et de la sous-estimation des bornes inférieures pour Max-SAT. Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.287-295, 2008. 〈inria-00292665〉

Partager

Métriques

Consultations de la notice

100

Téléchargements de fichiers

124