Certificats d'optimalité pour Max-SAT

Matthieu Py (1) , Mohamed Sami Cherif (1) , Djamal Habet (1)

1 COALA - COntraintes, ALgorithmes et Applications

Dans ce papier, on présente un outil, MS-Builder, qui génère des certificats pour le problème Max-SAT, en appelant itérativement un oracle SAT pour générer une réfutation par résolution de la formule qui est ensuite rendue valide pour Max-SAT et appliquée sur la formule. Ce procédé est répété jusqu'à ce que la formule restante devienne satisfiable. On propose également un outil, MS-Checker, capable de vérifier les certificats Max-SAT basés sur l'application de règles d'inférence Max-SAT. Cet article résume les travaux publiés à la conférence SAT 2021 [4].

Mots clés: Optimisation Combinatoire; Problème Max-SAT; Problème SAT; Certificats d'Optimalité

Domaines: Informatique [cs]

Matthieu Py, Mohamed Sami Cherif, Djamal Habet. Certificats d'optimalité pour Max-SAT. JFPC 2022, Jun 2022, Saint-Etienne, France. ⟨hal-03737729⟩