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

National audienceLe 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