Max-réfutations et oracles SAT

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

1 COALA - COntraintes, ALgorithmes et Applications

Adapter une réfutation par résolution en max-réfutation sans en augmenter considérablement sa taille est une question ouverte depuis l'introduction de la max-résolution. Cet article contribue à cette problématique en proposant un algorithme nommé algorithme de génération de remplaçants, capable d'adapter n'importe quelle réfutation par résolution en max-réfutation grâce à des appels à un oracle SAT. En particulier, on démontre que cet algorithme adapte efficacement les motifs en diamant, dont l'adaptation est exponentielle dans la littérature. Cet article résume le travail publié à la conférence ICTAI 2021 [3].

Mots clés: Max-SAT; Résolution; Max-Réfutation

Domaines: Informatique [cs]

Matthieu Py, Mohamed Sami Cherif, Djamal Habet. Max-réfutations et oracles SAT. JFPC 2022, Jun 2022, Saint-Etienne, France. ⟨hal-03737731⟩