Skip to Main content Skip to Navigation
Conference papers

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

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00292665
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Wednesday, July 2, 2008 - 12:13:30 PM
Last modification on : Monday, April 19, 2021 - 8:56:32 AM
Long-term archiving on: : Friday, May 28, 2010 - 11:04:41 PM

File

pages-287-295-article18.pdf
Files produced by the author(s)

Identifiers

  • 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. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, LINA - Université de Nantes - Ecole des Mines de Nantes, Jun 2008, Nantes, France. pp.287-295. ⟨inria-00292665⟩

Share

Metrics

Record views

133

Files downloads

658